diff -r a2719d9fe512 -r 0d22a6bf1fc6 src/Tools/isac/Specify/p-spec.sml
--- a/src/Tools/isac/Specify/p-spec.sml	Mon Jul 19 18:39:02 2021 +0200
+++ b/src/Tools/isac/Specify/p-spec.sml	Tue Jul 20 14:37:56 2021 +0200
@@ -80,13 +80,13 @@
     | NONE => (i, v, false, f, I_Model.Syn (UnparseC.term TermC.empty (*t  ..(t) has not been declared*))))
   | parsitm dI (i, v, b, f, I_Model.Syn str) =
     (case \<^try>\<open>
-        let val _ = (Thm.term_of o the o (TermC.parse dI)) str
+        let val _ = TermC.parseNEW'' dI str
         in (i, v, b ,f, I_Model.Par str) end\<close> of
       SOME x => x
     | NONE => (i, v, b, f, I_Model.Syn str))
   | parsitm dI (i, v, b, f, I_Model.Typ str) =
     (case \<^try>\<open>
-        let val _ = (Thm.term_of o the o (TermC.parse dI)) str
+        let val _ = TermC.parseNEW'' dI str
          in (i, v, b, f, I_Model.Par str) end\<close> of
       SOME x => x
     | NONE => (i, v, b, f, I_Model.Syn str))
@@ -157,13 +157,13 @@
 fun eq7 (f, d) (f', (d', _)) = f = f' andalso d = d';
 fun fstr2itm_ thy pbt (f, str) =
   let
-    val topt = TermC.parse thy str
+    val topt = TermC.parseNEW (ThyC.to_ctxt thy) str
   in
     case topt of
       NONE => ([], false, f, I_Model.Syn str)
     | SOME ct => 
 	    let
-	      val (d, ts) = (Input_Descript.split o Thm.term_of) ct
+	      val (d, ts) = (Input_Descript.split) ct
 	      val popt = find_first (eq7 (f, d)) pbt
 	    in
 	      case popt of