[isabelle-dev] Syntax.read_term ctxt

[bonzai at inode.at]

i studied isabelle/isar implementation, isabelle/isar reference manual  and the isabelle cookbook.
what am i still doing wrong ?

structure Data = Proof_Data
   (type T = term list
    fun init _ = []);
val ctxt =
   ProofContext.init_global @{theory} |>
   Data.map (fn trms => @{term "x::int"}::trms);
Data.get ctxt;

Syntax.read_term ctxt "x + 1 = 2";
(* we get Free ("x", "'a") etc, but would expect ...
val it =
    Const ("HOL.eq", "Int.int \<Rightarrow> Int.int \<Rightarrow> 
HOL.bool") $
      (Const ("Groups.plus_class.plus", "Int.int \<Rightarrow> Int.int 
\<Rightarrow> Int.int") $
        Free ("x", "Int.int") $ Const ("Groups.one_class.one", "Int.int")) $
      (Const ("Int.number_class.number_of", "Int.int \<Rightarrow> 
Int.int") $
        (Const ("Int.Bit0", "Int.int \<Rightarrow> Int.int") $
          (Const ("...", "Int.int \<Rightarrow> Int.int") $
            Const ("Int.Pls...", "Int.int")))):
    term
*)