1.1 --- a/src/Tools/isac/Specify/p-spec.sml	Mon Jul 19 18:39:02 2021 +0200
     1.2 +++ b/src/Tools/isac/Specify/p-spec.sml	Tue Jul 20 14:37:56 2021 +0200
     1.3 @@ -80,13 +80,13 @@
     1.4      | NONE => (i, v, false, f, I_Model.Syn (UnparseC.term TermC.empty (*t  ..(t) has not been declared*))))
     1.5    | parsitm dI (i, v, b, f, I_Model.Syn str) =
     1.6      (case \<^try>\<open>
     1.7 -        let val _ = (Thm.term_of o the o (TermC.parse dI)) str
     1.8 +        let val _ = TermC.parseNEW'' dI str
     1.9          in (i, v, b ,f, I_Model.Par str) end\<close> of
    1.10        SOME x => x
    1.11      | NONE => (i, v, b, f, I_Model.Syn str))
    1.12    | parsitm dI (i, v, b, f, I_Model.Typ str) =
    1.13      (case \<^try>\<open>
    1.14 -        let val _ = (Thm.term_of o the o (TermC.parse dI)) str
    1.15 +        let val _ = TermC.parseNEW'' dI str
    1.16           in (i, v, b, f, I_Model.Par str) end\<close> of
    1.17        SOME x => x
    1.18      | NONE => (i, v, b, f, I_Model.Syn str))
    1.19 @@ -157,13 +157,13 @@
    1.20  fun eq7 (f, d) (f', (d', _)) = f = f' andalso d = d';
    1.21  fun fstr2itm_ thy pbt (f, str) =
    1.22    let
    1.23 -    val topt = TermC.parse thy str
    1.24 +    val topt = TermC.parseNEW (ThyC.to_ctxt thy) str
    1.25    in
    1.26      case topt of
    1.27        NONE => ([], false, f, I_Model.Syn str)
    1.28      | SOME ct => 
    1.29  	    let
    1.30 -	      val (d, ts) = (Input_Descript.split o Thm.term_of) ct
    1.31 +	      val (d, ts) = (Input_Descript.split) ct
    1.32  	      val popt = find_first (eq7 (f, d)) pbt
    1.33  	    in
    1.34  	      case popt of