1.1 --- a/src/Tools/isac/BaseDefinitions/termC.sml Tue Jul 20 14:37:56 2021 +0200
1.2 +++ b/src/Tools/isac/BaseDefinitions/termC.sml Tue Jul 27 11:21:14 2021 +0200
1.3 @@ -68,9 +68,12 @@
1.4 val mk_var_op_num: term -> string -> typ -> typ -> int -> term
1.5
1.6 val matches: theory -> term -> term -> bool
1.7 + val parse: theory -> string -> cterm option
1.8 + val parseN: theory -> string -> cterm option
1.9 val parseNEW: Proof.context -> string -> term option
1.10 val parseNEW': Proof.context -> string -> term
1.11 val parseNEW'': theory -> string -> term
1.12 + val parseold: theory -> string -> cterm option
1.13 val parse_strict: theory -> string -> term
1.14 val parse_patt: theory -> string -> term
1.15 val perm: term -> term -> bool
1.16 @@ -530,21 +533,21 @@
1.17 | typ_a2real (Abs(s,T,t)) = Abs(s, T, typ_a2real t)
1.18 | typ_a2real (t1 $ t2) = (typ_a2real t1) $ (typ_a2real t2);
1.19
1.20 -(* TODO clarify parse with Test_Isac * )
1.21 +(* TODO clarify parse with Test_Isac *)
1.22 fun parseold thy str = (* before 2002 *)
1.23 \<^try>\<open>
1.24 let val t = Syntax.read_term_global thy str
1.25 in Thm.global_cterm_of thy t end\<close>;
1.26 fun parseN thy str = (* introduced 2002 *)
1.27 \<^try>\<open>
1.28 - let val t = Syntax.read_term_global thy str
1.29 + let val t = (*(typ_a2real o numbers_to_string)*) (Syntax.read_term_global thy str)
1.30 in Thm.global_cterm_of thy t end\<close>;
1.31
1.32 +fun parse_strict thy str = typ_a2real (Syntax.read_term_global thy str);
1.33 fun parse thy str = (* introduced 2010 *)
1.34 \<^try>\<open>
1.35 let val t = parse_strict thy str
1.36 in Thm.global_cterm_of thy t end\<close>;
1.37 -*)
1.38
1.39 (*WN110317 parseNEW will replace parse after introduction of ctxt completed*)
1.40 fun parseNEW ctxt str = \<^try>\<open>Syntax.read_term ctxt str\<close>;
1.41 @@ -556,7 +559,6 @@
1.42 case parseNEW (ThyC.to_ctxt thy) str of
1.43 SOME t => t
1.44 | NONE => raise TERM ("NO parseNEW'' for " ^ str, [])
1.45 -fun parse_strict thy str = (*typ_a2real*) (parseNEW'' thy str);
1.46
1.47 (* parse term patterns; Var ("v",_), i.e. "?v", are required for instantiation
1.48 WN130613 probably compare to