[isabelle-dev] Syntax.read_term ctxt

[Makarius]

On Thu, 3 Mar 2011, bonzai at inode.at wrote:

> 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
> *)

I cannot reproduce the problem.  This is the output of ML toplevel 
declarations produced here:

structure Data : PROOF_DATA
val ctxt = <context>: Proof.context
val it = [Free ("x", "Int.int")]: Data.T
val it =
    Const ("HOL.eq", "'a \<Rightarrow> 'a \<Rightarrow> HOL.bool") $
      (Const ("Groups.plus_class.plus", "'a \<Rightarrow> 'a \<Rightarrow> 'a") $ Free ("x", "'a") $
        Const ("Groups.one_class.one", "'a")) $
      (Const ("Int.number_class.number_of", "Int.int \<Rightarrow> 'a") $
        (Const ("Int.Bit0", "Int.int \<Rightarrow> Int.int") $
          (Const ("...", "Int.int \<Rightarrow> Int.int") $ Const ("Int.Pls...", "Int.int")))):
    term


Further notes:

   * trm, trms are a bad naming convention for terms; use t, ts or tm, tms
     instead.

   * You can ask questions about Isabelle/ML on the isabelle-users mailing
     list.  isabelle-dev means you are hooked on unofficial repository
     versions for some reason, in which case you should also say which
     one it is (e.g. via isabelle version -i).


 	Makarius