1.1 --- a/src/Tools/isac/Specify/p-spec.sml	Mon Jan 30 12:38:17 2023 +0100
     1.2 +++ b/src/Tools/isac/Specify/p-spec.sml	Tue Jan 31 10:49:17 2023 +0100
     1.3 @@ -140,7 +140,9 @@
     1.4    let 
     1.5       val ctxt = ThyC.get_theory dI |> Proof_Context.init_global;
     1.6    in
     1.7 -    case TermC.parseNEW ctxt ct of
     1.8 +    (*/------------ replace by ParseC.term_position ------------------\*)
     1.9 +    case ParseC.term_opt ctxt ct of
    1.10 +    (*\------------ replace by ParseC.term_position ------------------/*)
    1.11  	    NONE => (0, [], false, sel, I_Model.Syn ct)
    1.12  	  | SOME t =>
    1.13  	    (case O_Model.contains ctxt sel oris t of
    1.14 @@ -158,7 +160,9 @@
    1.15  fun eq7 (f, d) (f', (d', _)) = f = f' andalso d = d';
    1.16  fun fstr2itm_ thy pbt (f, str) =
    1.17    let
    1.18 -    val topt = TermC.parseNEW (Proof_Context.init_global thy) str
    1.19 +    (*/------------ replace by ParseC.term_position ? ------------\*)
    1.20 +    val topt = ParseC.term_opt (Proof_Context.init_global thy) str
    1.21 +    (*\------------ replace by ParseC.term_position ? ------------/*)
    1.22    in
    1.23      case topt of
    1.24        NONE => ([], false, f, I_Model.Syn str)