1.1 --- a/src/Tools/isac/Specify/m-match.sml	Wed Jan 11 09:23:18 2023 +0100
     1.2 +++ b/src/Tools/isac/Specify/m-match.sml	Wed Jan 11 11:38:01 2023 +0100
     1.3 @@ -153,6 +153,8 @@
     1.4     an type-error is reported immediately, raises an exn, 
     1.5     subsequent handling of exn provides 2nd part of error message *)
     1.6  fun mtc thy (str, (dsc, _)) (ty $ var) =
     1.7 +    let val ctxt = Proof_Context.init_global thy
     1.8 +    in
     1.9      ((Thm.global_cterm_of thy (dsc $ var);(*type check*)
    1.10        SOME (([1], str, dsc, (*[var]*)
    1.11  	    Input_Descript.split' (dsc, var))) (*:ori without leading #*))
    1.12 @@ -160,16 +162,19 @@
    1.13  	      (tracing (dashs 70 ^ "\n"
    1.14  	        ^ "*** ERROR while creating the items for the model of the ->problem\n"
    1.15  	        ^ "*** from the ->stac with ->typeconstructor in arglist:\n"
    1.16 -	        ^ "*** item (->description ->value): " ^ UnparseC.term dsc ^ " " ^ UnparseC.term var ^ "\n"
    1.17 -	        ^ "*** description: " ^ TermC.term_detail2str dsc
    1.18 -	        ^ "*** value: " ^ TermC.term_detail2str var
    1.19 -	        ^ "*** typeconstructor in script: " ^ TermC.term_detail2str ty
    1.20 +	        ^ "*** item (->description ->value): " ^ UnparseC.term_in_ctxt ctxt dsc ^ " " ^ UnparseC.term_in_ctxt ctxt var ^ "\n"
    1.21 +	        ^ "*** description: " ^ TermC.string_of_detail ctxt dsc
    1.22 +	        ^ "*** value: " ^ TermC.string_of_detail ctxt var
    1.23 +	        ^ "*** typeconstructor in script: " ^ TermC.string_of_detail ctxt ty
    1.24  	        ^ "*** checked by theory: " ^ Context.theory_name thy ^ "\n"
    1.25  	        ^ "*** " ^ dots 66);
    1.26            writeln (@{make_string} e);
    1.27            Exn.reraise e; (*raise ERROR "actual args do not match formal args";FIXXXME.WN100916*)
    1.28        NONE))
    1.29 -  | mtc _ _ t = raise ERROR ("mtc: uncovered case with" ^ UnparseC.term t)
    1.30 +    end
    1.31 +  | mtc thy _ t =
    1.32 +    let val ctxt = Proof_Context.init_global thy
    1.33 +    in raise ERROR ("mtc: uncovered case with" ^ UnparseC.term_in_ctxt ctxt t) end
    1.34  
    1.35  (* match each pat of the model-pattern with an actual argument;
    1.36     precondition: copy-named vars are filtered out            *)