1.1 --- a/src/Tools/isac/Specify/p-spec.sml	Sat Feb 04 16:20:45 2023 +0100
     1.2 +++ b/src/Tools/isac/Specify/p-spec.sml	Sat Feb 04 16:49:08 2023 +0100
     1.3 @@ -77,7 +77,8 @@
     1.4            (*t his ^^^^^^^^^^^^ should raise the exn on unability of re-parsing dts *)
     1.5          in itm end\<close> of
     1.6        SOME x => x
     1.7 -    | NONE => (i, v, false, f, I_Model.Syn (UnparseC.term TermC.empty (*t  ..(t) has not been declared*))))
     1.8 +    | NONE =>
     1.9 +      (i, v, false, f, I_Model.Syn (UnparseC.term_in_thy thy TermC.empty (*t  ..(t) has not been declared*))))
    1.10    | parsitm _ (i, v, b, f, I_Model.Syn str) =
    1.11      (case \<^try>\<open>
    1.12          let val _ = Syntax.read_term\<^context> str
    1.13 @@ -97,7 +98,7 @@
    1.14          (*this    ^ should raise the exn on unability of re-parsing dts*)
    1.15          in itm end\<close> of
    1.16        SOME x => x
    1.17 -    | NONE => (i, v, false, f, I_Model.Syn (UnparseC.term TermC.empty (*t  ..(t) has not been declared*))))
    1.18 +    | NONE => (i, v, false, f, I_Model.Syn (UnparseC.term_in_thy thy TermC.empty (*t  ..(t) has not been declared*))))
    1.19    | parsitm thy (itm as (i, v, _, f, I_Model.Sup (d, ts))) =
    1.20      (case \<^try>\<open>
    1.21          let val t = Input_Descript.join (d,ts);
    1.22 @@ -105,7 +106,7 @@
    1.23          (*this    ^ should raise the exn on unability of re-parsing dts*)
    1.24          in itm end\<close> of
    1.25        SOME x => x
    1.26 -    | NONE => (i, v, false, f, I_Model.Syn (UnparseC.term TermC.empty (*t  ..(t) has not been declared*))))
    1.27 +    | NONE => (i, v, false, f, I_Model.Syn (UnparseC.term_in_thy thy TermC.empty (*t  ..(t) has not been declared*))))
    1.28    | parsitm thy (itm as (i, v, _, f, I_Model.Mis (d, t'))) =
    1.29      (case \<^try>\<open>
    1.30          let val t = d $ t';
    1.31 @@ -113,7 +114,7 @@
    1.32          (*this    ^ should raise the exn on unability of re-parsing dts*)
    1.33          in itm end\<close> of
    1.34        SOME x => x
    1.35 -    | NONE => (i, v, false, f, I_Model.Syn (UnparseC.term TermC.empty (*t  ..(t) has not been declared*))))
    1.36 +    | NONE => (i, v, false, f, I_Model.Syn (UnparseC.term_in_thy thy TermC.empty (*t  ..(t) has not been declared*))))
    1.37    | parsitm thy (itm as (_, _, _, _, I_Model.Par _)) = 
    1.38      raise ERROR ("parsitm (" ^ I_Model.single_to_string (Proof_Context.init_global thy) itm ^
    1.39        "): Par should be internal");