1.1 --- a/src/HOL/Tools/TFL/tfl.ML	Fri Aug 28 18:23:24 2009 +0200
     1.2 +++ b/src/HOL/Tools/TFL/tfl.ML	Fri Aug 28 21:04:03 2009 +0200
     1.3 @@ -8,7 +8,7 @@
     1.4  sig
     1.5    val trace: bool ref
     1.6    val trace_thms: string -> thm list -> unit
     1.7 -  val trace_cterms: string -> cterm list -> unit
     1.8 +  val trace_cterm: string -> cterm -> unit
     1.9    type pattern
    1.10    val mk_functional: theory -> term list -> {functional: term, pats: pattern list}
    1.11    val wfrec_definition0: theory -> string -> term -> term -> theory * thm
    1.12 @@ -296,7 +296,7 @@
    1.13              raise TFL_ERR "no_repeat_vars"
    1.14                            (quote (#1 (dest_Free v)) ^
    1.15                            " occurs repeatedly in the pattern " ^
    1.16 -                          quote (Display.string_of_cterm (Thry.typecheck thy pat)))
    1.17 +                          quote (Syntax.string_of_term_global thy pat))
    1.18           else check rst
    1.19   in check (FV_multiset pat)
    1.20   end;
    1.21 @@ -912,9 +912,10 @@
    1.22    if !trace then writeln (cat_lines (s :: map Display.string_of_thm_without_context L))
    1.23    else ();
    1.24  
    1.25 -fun trace_cterms s L =
    1.26 -  if !trace then writeln (cat_lines (s :: map Display.string_of_cterm L))
    1.27 -  else ();;
    1.28 +fun trace_cterm s ct =
    1.29 +  if !trace then
    1.30 +    writeln (cat_lines [s, Syntax.string_of_term_global (Thm.theory_of_cterm ct) (Thm.term_of ct)])
    1.31 +  else ();
    1.32  
    1.33  
    1.34  fun postprocess strict {wf_tac, terminator, simplifier} theory {rules,induction,TCs} =
    1.35 @@ -942,7 +943,7 @@
    1.36  
    1.37     fun simplify_tc tc (r,ind) =
    1.38         let val tc1 = tych tc
    1.39 -           val _ = trace_cterms "TC before simplification: " [tc1]
    1.40 +           val _ = trace_cterm "TC before simplification: " tc1
    1.41             val tc_eq = simplifier tc1
    1.42             val _ = trace_thms "result: " [tc_eq]
    1.43         in