diff -r ef24b1eed505 -r e5884e07a292 src/Tools/isac/Specify/p-spec.sml
--- a/src/Tools/isac/Specify/p-spec.sml	Sat Feb 04 16:20:45 2023 +0100
+++ b/src/Tools/isac/Specify/p-spec.sml	Sat Feb 04 16:49:08 2023 +0100
@@ -77,7 +77,8 @@
           (*t his ^^^^^^^^^^^^ should raise the exn on unability of re-parsing dts *)
         in itm end\<close> of
       SOME x => x
-    | NONE => (i, v, false, f, I_Model.Syn (UnparseC.term TermC.empty (*t  ..(t) has not been declared*))))
+    | NONE =>
+      (i, v, false, f, I_Model.Syn (UnparseC.term_in_thy thy TermC.empty (*t  ..(t) has not been declared*))))
   | parsitm _ (i, v, b, f, I_Model.Syn str) =
     (case \<^try>\<open>
         let val _ = Syntax.read_term\<^context> str
@@ -97,7 +98,7 @@
         (*this    ^ should raise the exn on unability of re-parsing dts*)
         in itm end\<close> of
       SOME x => x
-    | NONE => (i, v, false, f, I_Model.Syn (UnparseC.term TermC.empty (*t  ..(t) has not been declared*))))
+    | NONE => (i, v, false, f, I_Model.Syn (UnparseC.term_in_thy thy TermC.empty (*t  ..(t) has not been declared*))))
   | parsitm thy (itm as (i, v, _, f, I_Model.Sup (d, ts))) =
     (case \<^try>\<open>
         let val t = Input_Descript.join (d,ts);
@@ -105,7 +106,7 @@
         (*this    ^ should raise the exn on unability of re-parsing dts*)
         in itm end\<close> of
       SOME x => x
-    | NONE => (i, v, false, f, I_Model.Syn (UnparseC.term TermC.empty (*t  ..(t) has not been declared*))))
+    | NONE => (i, v, false, f, I_Model.Syn (UnparseC.term_in_thy thy TermC.empty (*t  ..(t) has not been declared*))))
   | parsitm thy (itm as (i, v, _, f, I_Model.Mis (d, t'))) =
     (case \<^try>\<open>
         let val t = d $ t';
@@ -113,7 +114,7 @@
         (*this    ^ should raise the exn on unability of re-parsing dts*)
         in itm end\<close> of
       SOME x => x
-    | NONE => (i, v, false, f, I_Model.Syn (UnparseC.term TermC.empty (*t  ..(t) has not been declared*))))
+    | NONE => (i, v, false, f, I_Model.Syn (UnparseC.term_in_thy thy TermC.empty (*t  ..(t) has not been declared*))))
   | parsitm thy (itm as (_, _, _, _, I_Model.Par _)) = 
     raise ERROR ("parsitm (" ^ I_Model.single_to_string (Proof_Context.init_global thy) itm ^
       "): Par should be internal");