1.1 --- a/src/Tools/isac/BaseDefinitions/termC.sml Mon Sep 27 20:24:24 2021 +0200
1.2 +++ b/src/Tools/isac/BaseDefinitions/termC.sml Wed Sep 29 18:56:38 2021 +0200
1.3 @@ -70,13 +70,15 @@
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 +
1.10 val parseNEW: Proof.context -> string -> term option
1.11 val parseNEW': Proof.context -> string -> term
1.12 val parseNEW'': theory -> string -> term
1.13 val parseold: theory -> string -> cterm option
1.14 + val parseN: theory -> string -> cterm option
1.15 val parse_strict: theory -> string -> term
1.16 + val parse: theory -> string -> cterm option
1.17 +
1.18 val parse_patt: theory -> string -> term
1.19 val perm: term -> term -> bool
1.20
1.21 @@ -543,6 +545,17 @@
1.22 | typ_a2real (Abs(s,T,t)) = Abs(s, T, typ_a2real t)
1.23 | typ_a2real (t1 $ t2) = (typ_a2real t1) $ (typ_a2real t2);
1.24
1.25 +(*WN110317 parseNEW will replace parse after introduction of ctxt completed*)
1.26 +fun parseNEW ctxt str = \<^try>\<open>Syntax.read_term ctxt str\<close>;
1.27 +fun parseNEW' ctxt str =
1.28 + case parseNEW ctxt str of
1.29 + SOME t => t
1.30 + | NONE => raise TERM ("NO parseNEW' for " ^ str, [])
1.31 +fun parseNEW'' thy str =
1.32 + case parseNEW (Proof_Context.init_global thy) str of
1.33 + SOME t => t
1.34 + | NONE => raise TERM ("NO parseNEW'' for " ^ str, [])
1.35 +
1.36 (* TODO clarify parse with Test_Isac *)
1.37 fun parseold thy str = (* before 2002 *)
1.38 \<^try>\<open>
1.39 @@ -559,17 +572,6 @@
1.40 let val t = parse_strict thy str
1.41 in Thm.global_cterm_of thy t end\<close>;
1.42
1.43 -(*WN110317 parseNEW will replace parse after introduction of ctxt completed*)
1.44 -fun parseNEW ctxt str = \<^try>\<open>Syntax.read_term ctxt str\<close>;
1.45 -fun parseNEW' ctxt str =
1.46 - case parseNEW ctxt str of
1.47 - SOME t => t
1.48 - | NONE => raise TERM ("NO parseNEW' for " ^ str, [])
1.49 -fun parseNEW'' thy str =
1.50 - case parseNEW (Proof_Context.init_global thy) str of
1.51 - SOME t => t
1.52 - | NONE => raise TERM ("NO parseNEW'' for " ^ str, [])
1.53 -
1.54 (* parse term patterns; Var ("v",_), i.e. "?v", are required for instantiation
1.55 WN130613 probably compare to
1.56 http://www.mail-archive.com/isabelle-dev@mailbroy.informatik.tu-muenchen.de/msg04249.html*)