diff -r b2ff1902420f -r 06ec8abfd3bc src/Tools/isac/Specify/m-match.sml
--- a/src/Tools/isac/Specify/m-match.sml	Wed Jan 11 09:23:18 2023 +0100
+++ b/src/Tools/isac/Specify/m-match.sml	Wed Jan 11 11:38:01 2023 +0100
@@ -153,6 +153,8 @@
    an type-error is reported immediately, raises an exn, 
    subsequent handling of exn provides 2nd part of error message *)
 fun mtc thy (str, (dsc, _)) (ty $ var) =
+    let val ctxt = Proof_Context.init_global thy
+    in
     ((Thm.global_cterm_of thy (dsc $ var);(*type check*)
       SOME (([1], str, dsc, (*[var]*)
 	    Input_Descript.split' (dsc, var))) (*:ori without leading #*))
@@ -160,16 +162,19 @@
 	      (tracing (dashs 70 ^ "\n"
 	        ^ "*** ERROR while creating the items for the model of the ->problem\n"
 	        ^ "*** from the ->stac with ->typeconstructor in arglist:\n"
-	        ^ "*** item (->description ->value): " ^ UnparseC.term dsc ^ " " ^ UnparseC.term var ^ "\n"
-	        ^ "*** description: " ^ TermC.term_detail2str dsc
-	        ^ "*** value: " ^ TermC.term_detail2str var
-	        ^ "*** typeconstructor in script: " ^ TermC.term_detail2str ty
+	        ^ "*** item (->description ->value): " ^ UnparseC.term_in_ctxt ctxt dsc ^ " " ^ UnparseC.term_in_ctxt ctxt var ^ "\n"
+	        ^ "*** description: " ^ TermC.string_of_detail ctxt dsc
+	        ^ "*** value: " ^ TermC.string_of_detail ctxt var
+	        ^ "*** typeconstructor in script: " ^ TermC.string_of_detail ctxt ty
 	        ^ "*** checked by theory: " ^ Context.theory_name thy ^ "\n"
 	        ^ "*** " ^ dots 66);
           writeln (@{make_string} e);
           Exn.reraise e; (*raise ERROR "actual args do not match formal args";FIXXXME.WN100916*)
       NONE))
-  | mtc _ _ t = raise ERROR ("mtc: uncovered case with" ^ UnparseC.term t)
+    end
+  | mtc thy _ t =
+    let val ctxt = Proof_Context.init_global thy
+    in raise ERROR ("mtc: uncovered case with" ^ UnparseC.term_in_ctxt ctxt t) end
 
 (* match each pat of the model-pattern with an actual argument;
    precondition: copy-named vars are filtered out            *)