src/HOL/Tools/TFL/tfl.ML

        | 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 (string_of_cterm (Thry.typecheck thy pat)))
+                          quote (Display.string_of_cterm (Thry.typecheck thy pat)))
          else check rst
  in check (FV_multiset pat)
  end;
 
 fun dest_atom (Free p) = p

      val R1 = S.rand WFR
      val f = #lhs(S.dest_eq proto_def)
      val (extractants,TCl) = ListPair.unzip extracta
      val dummy = if !trace
                  then (writeln "Extractants = ";
-                       prths extractants;
+                       Display.prths extractants;
                        ())
                  else ()
      val TCs = foldr (gen_union (op aconv)) [] TCl
      val full_rqt = WFR::TCs
      val R' = S.mk_select{Bvar=R1, Body=S.list_mk_conj full_rqt}

      val ([def0], theory) =
        thy
        |> PureThy.add_defs_i false
             [Thm.no_attributes (fid ^ "_def", defn)]
      val def = Thm.freezeT def0;
-     val dummy = if !trace then writeln ("DEF = " ^ string_of_thm def)
+     val dummy = if !trace then writeln ("DEF = " ^ Display.string_of_thm def)
                            else ()
      (* val fconst = #lhs(S.dest_eq(concl def))  *)
      val tych = Thry.typecheck theory
      val full_rqt_prop = map (Dcterm.mk_prop o tych) full_rqt
          (*lcp: a lot of object-logic inference to remove*)
      val baz = R.DISCH_ALL
                  (fold_rev R.DISCH full_rqt_prop
                   (R.LIST_CONJ extractants))
-     val dum = if !trace then writeln ("baz = " ^ string_of_thm baz)
+     val dum = if !trace then writeln ("baz = " ^ Display.string_of_thm baz)
                            else ()
      val f_free = Free (fid, fastype_of f)  (*'cos f is a Const*)
      val SV' = map tych SV;
      val SVrefls = map reflexive SV'
      val def0 = (fold (fn x => fn th => R.rbeta(combination th x))

 fun elim_tc tcthm (rule,induction) =
    (R.MP rule tcthm, R.PROVE_HYP tcthm induction)
 
 
 fun trace_thms s L =
-  if !trace then writeln (cat_lines (s :: map string_of_thm L))
+  if !trace then writeln (cat_lines (s :: map Display.string_of_thm L))
   else ();
 
 fun trace_cterms s L =
-  if !trace then writeln (cat_lines (s :: map string_of_cterm L))
+  if !trace then writeln (cat_lines (s :: map Display.string_of_cterm L))
   else ();;
 
 
 fun postprocess strict {wf_tac, terminator, simplifier} theory {rules,induction,TCs} =
 let val tych = Thry.typecheck theory