1.1 --- a/src/Tools/isac/BaseDefinitions/termC.sml	Tue Aug 10 10:27:15 2021 +0200
     1.2 +++ b/src/Tools/isac/BaseDefinitions/termC.sml	Tue Aug 10 11:01:18 2021 +0200
     1.3 @@ -557,7 +557,7 @@
     1.4      SOME t => t
     1.5    | NONE => raise TERM ("NO parseNEW' for " ^ str, [])
     1.6  fun parseNEW'' thy str =
     1.7 -  case parseNEW (ThyC.to_ctxt thy) str of
     1.8 +  case parseNEW (Proof_Context.init_global thy) str of
     1.9      SOME t => t
    1.10    | NONE => raise TERM ("NO parseNEW'' for " ^ str, [])
    1.11  
    1.12 @@ -565,7 +565,7 @@
    1.13    WN130613 probably compare to 
    1.14    http://www.mail-archive.com/isabelle-dev@mailbroy.informatik.tu-muenchen.de/msg04249.html*)
    1.15  fun parse_patt thy str = (thy, str)
    1.16 -  |>> ThyC.to_ctxt 
    1.17 +  |>> Proof_Context.init_global
    1.18    |-> Proof_Context.read_term_pattern
    1.19  (*|> numbers_to_string   TODO drop*)
    1.20    |> typ_a2real;       (*TODO drop*)