1.1 --- a/src/Tools/isac/Specify/p-spec.sml	Tue May 24 12:57:47 2022 +0200
     1.2 +++ b/src/Tools/isac/Specify/p-spec.sml	Tue May 24 16:47:31 2022 +0200
     1.3 @@ -154,17 +154,17 @@
     1.4          else (i, v, false, sel, I_Model.Sup (d, ts)))
     1.5     end
     1.6  
     1.7 -(* generate preliminary itm_ from a strin (with field "#Given" etc.) *)
     1.8 +(* generate preliminary itm_ from a string (with field "#Given" etc.) *)
     1.9  fun eq7 (f, d) (f', (d', _)) = f = f' andalso d = d';
    1.10  fun fstr2itm_ thy pbt (f, str) =
    1.11    let
    1.12 -    val topt = TermC.parse thy str
    1.13 +    val topt = TermC.parseNEW (Proof_Context.init_global thy) str
    1.14    in
    1.15      case topt of
    1.16        NONE => ([], false, f, I_Model.Syn str)
    1.17      | SOME ct => 
    1.18  	    let
    1.19 -	      val (d, ts) = (Input_Descript.split o Thm.term_of) ct
    1.20 +	      val (d, ts) = Input_Descript.split ct
    1.21  	      val popt = find_first (eq7 (f, d)) pbt
    1.22  	    in
    1.23  	      case popt of