1.1 --- a/src/Tools/isac/BaseDefinitions/termC.sml	Wed Sep 29 19:26:12 2021 +0200
     1.2 +++ b/src/Tools/isac/BaseDefinitions/termC.sml	Wed Sep 29 19:34:32 2021 +0200
     1.3 @@ -74,7 +74,6 @@
     1.4    val parseNEW: Proof.context -> string -> term option
     1.5    val parseNEW': Proof.context -> string -> term
     1.6    val parseNEW'': theory -> string -> term
     1.7 -  val parseN: theory -> string -> cterm option
     1.8    val parse_strict: theory -> string -> term
     1.9    val parse: theory -> string -> cterm option
    1.10  
    1.11 @@ -556,11 +555,6 @@
    1.12    | NONE => raise TERM ("NO parseNEW'' for " ^ str, [])
    1.13  
    1.14  (* TODO clarify parse with Test_Isac *)
    1.15 -fun parseN thy str = (* introduced 2002 *)
    1.16 -  \<^try>\<open>
    1.17 -    let val t = (*(typ_a2real o numbers_to_string)*) (Syntax.read_term_global thy str)
    1.18 -    in Thm.global_cterm_of thy t end\<close>;
    1.19 -
    1.20  fun parse_strict thy str = typ_a2real (Syntax.read_term_global thy str);
    1.21  fun parse thy str = (* introduced 2010 *)
    1.22    \<^try>\<open>

     2.1 --- a/src/Tools/isac/ProgLang/Auto_Prog.thy	Wed Sep 29 19:26:12 2021 +0200
     2.2 +++ b/src/Tools/isac/ProgLang/Auto_Prog.thy	Wed Sep 29 19:34:32 2021 +0200
     2.3 @@ -110,24 +110,24 @@
     2.4  (*WN060605 script-arg (t_::'z) and "Free (t_, 'a)" at end of body are inconsistent !!!*)
     2.5  val (FunID_Term $ _) = Program.prep_program @{thm auto_generated.simps}
     2.6  val (FunID_Term_Bdv $ _) = Program.prep_program @{thm auto_generated_inst.simps}
     2.7 -val Repeat $ _ = (TermC.inst_abs o Thm.term_of o the o (TermC.parseN @{theory})) 
     2.8 +val Repeat $ _ = (TermC.inst_abs o (TermC.parseNEW'' @{theory}))
     2.9  	"Repeat (Rewrite ''real_diff_minus'' t)";
    2.10 -val Try $ _ = (TermC.inst_abs o Thm.term_of o the o (TermC.parseN @{theory})) 
    2.11 +val Try $ _ = (TermC.inst_abs o (TermC.parseNEW'' @{theory}))
    2.12  	"Try (Rewrite ''real_diff_minus'' t)";
    2.13 -val Cal $ _ = (TermC.inst_abs o Thm.term_of o the o (TermC.parseN @{theory})) 
    2.14 +val Cal $ _ = (TermC.inst_abs o (TermC.parseNEW'' @{theory}))
    2.15  	"Calculate ''PLUS''";
    2.16 -val Ca1 $ _ = (TermC.inst_abs o Thm.term_of o the o (TermC.parseN @{theory})) 
    2.17 +val Ca1 $ _ = (TermC.inst_abs o (TermC.parseNEW'' @{theory}))
    2.18  	"Calculate1 ''PLUS''";
    2.19 -val Rew $ _ $ _ = (TermC.inst_abs o Thm.term_of o the o (TermC.parseN @{theory})) 
    2.20 +val Rew $ _ $ _ = (TermC.inst_abs o (TermC.parseNEW'' @{theory}))
    2.21  	"Rewrite ''real_diff_minus'' t";
    2.22  (*this is specific to FunHead_inst ...*)
    2.23 -val Rew_Inst $ Subs $ _ = (TermC.inst_abs o Thm.term_of o the o (TermC.parseN @{theory})) 
    2.24 +val Rew_Inst $ Subs $ _ = (TermC.inst_abs o (TermC.parseNEW'' @{theory}))
    2.25  	"Rewrite_Inst [(''bdv'',v)] ''real_diff_minus''";
    2.26 -val Rew_Set $ _ = (TermC.inst_abs o Thm.term_of o the o (TermC.parseN @{theory})) 
    2.27 +val Rew_Set $ _ = (TermC.inst_abs o (TermC.parseNEW'' @{theory}))
    2.28  	"Rewrite_Set ''real_diff_minus''";
    2.29 -val Rew_Set_Inst $ _ $ _ = (TermC.inst_abs o Thm.term_of o the o (TermC.parseN @{theory})) 
    2.30 +val Rew_Set_Inst $ _ $ _ = (TermC.inst_abs o (TermC.parseNEW'' @{theory}))
    2.31  	"Rewrite_Set_Inst [(''bdv'',v)] ''real_diff_minus''";
    2.32 -val SEq $ _ $ _ $ _ = (TermC.inst_abs o Thm.term_of o the o (TermC.parseN @{theory})) 
    2.33 +val SEq $ _ $ _ $ _ = (TermC.inst_abs o (TermC.parseNEW'' @{theory}))
    2.34  	"  ((Try (Repeat (Rewrite ''real_diff_minus''))) #>  \
    2.35          \   (Try (Repeat (Rewrite ''add.commute''))) #> \
    2.36          \   (Try (Repeat (Rewrite ''mult_commute'')))) t"; (*has not yet been needed*)