src/HOL/Tools/TFL/tfl.ML

 
 signature PRIM =
 sig
   val trace: bool ref
   val trace_thms: string -> thm list -> unit
-  val trace_cterms: string -> cterm list -> unit
+  val trace_cterm: string -> cterm -> unit
   type pattern
   val mk_functional: theory -> term list -> {functional: term, pats: pattern list}
   val wfrec_definition0: theory -> string -> term -> term -> theory * thm
   val post_definition: thm list -> theory * (thm * pattern list) ->
    {rules: thm,

        | check (v::rst) =
          if member (op aconv) rst v then
             raise TFL_ERR "no_repeat_vars"
                           (quote (#1 (dest_Free v)) ^
                           " occurs repeatedly in the pattern " ^
-                          quote (Display.string_of_cterm (Thry.typecheck thy pat)))
+                          quote (Syntax.string_of_term_global thy pat))
          else check rst
  in check (FV_multiset pat)
  end;
 
 fun dest_atom (Free p) = p

 
 fun trace_thms s L =
   if !trace then writeln (cat_lines (s :: map Display.string_of_thm_without_context L))
   else ();
 
-fun trace_cterms s L =
-  if !trace then writeln (cat_lines (s :: map Display.string_of_cterm L))
-  else ();;
+fun trace_cterm s ct =
+  if !trace then
+    writeln (cat_lines [s, Syntax.string_of_term_global (Thm.theory_of_cterm ct) (Thm.term_of ct)])
+  else ();
 
 
 fun postprocess strict {wf_tac, terminator, simplifier} theory {rules,induction,TCs} =
 let val tych = Thry.typecheck theory
     val prove = R.prove strict;

     *   3. replace tc by tc' in both the rules and the induction theorem.
     *---------------------------------------------------------------------*)
 
    fun simplify_tc tc (r,ind) =
        let val tc1 = tych tc
-           val _ = trace_cterms "TC before simplification: " [tc1]
+           val _ = trace_cterm "TC before simplification: " tc1
            val tc_eq = simplifier tc1
            val _ = trace_thms "result: " [tc_eq]
        in
        elim_tc (R.MATCH_MP Thms.eqT tc_eq) (r,ind)
        handle U.ERR _ =>