src/HOL/Tools/TFL/tfl.ML

            wfrec_eqns thy fid tflCongs eqns
      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 = ";
-                       Display.prths extractants;
-                       ())
+                 then writeln (cat_lines ("Extractants =" ::
+                  map (Display.string_of_thm_global thy) extractants))
                  else ()
      val TCs = List.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 R'abs = S.rand R'

      val ([def0], theory) =
        thy
        |> PureThy.add_defs false
             [Thm.no_attributes (Binding.name (fid ^ "_def"), defn)]
      val def = Thm.freezeT def0;
-     val dummy = if !trace then writeln ("DEF = " ^ Display.string_of_thm def)
-                           else ()
+     val dummy =
+       if !trace then writeln ("DEF = " ^ Display.string_of_thm_global theory 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 = " ^ Display.string_of_thm baz)
+     val dum = if !trace then writeln ("baz = " ^ Display.string_of_thm_global theory 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 Display.string_of_thm 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 ();;