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