1.1 --- a/src/Tools/isac/BaseDefinitions/termC.sml	Fri May 08 11:01:11 2020 +0200
     1.2 +++ b/src/Tools/isac/BaseDefinitions/termC.sml	Fri May 08 18:30:21 2020 +0200
     1.3 @@ -67,6 +67,7 @@
     1.4    val parseN: theory -> string -> cterm option
     1.5    val parseNEW: Proof.context -> string -> term option
     1.6    val parseNEW': Proof.context -> string -> term
     1.7 +  val parseNEW'': theory -> string -> term
     1.8    val parseold: theory -> string -> cterm option
     1.9    val parse_patt: theory -> string -> term
    1.10    val perm: term -> term -> bool
    1.11 @@ -506,6 +507,10 @@
    1.12    case parseNEW ctxt str of
    1.13      SOME t => t
    1.14    | NONE => raise TERM ("NO parseNEW' for " ^ str, [])
    1.15 +fun parseNEW'' thy str =
    1.16 +  case parseNEW (ThyC.to_ctxt thy) str of
    1.17 +    SOME t => t
    1.18 +  | NONE => raise TERM ("NO parseNEW'' for " ^ str, [])
    1.19  
    1.20  (* parse term patterns; Var ("v",_), i.e. "?v", are required for instantiation
    1.21    WN130613 probably compare to