src/HOL/Tools/res_axioms.ML

 val [g_C,f_C] = map (cterm_of @{theory}) (term_vars (prop_of abs_C));
 val [f_S,g_S] = map (cterm_of @{theory}) (term_vars (prop_of abs_S));
 
 (*FIXME: requires more use of cterm constructors*)
 fun abstract ct =
-  let val _ = Output.debug (fn()=>"  abstraction: " ^ string_of_cterm ct)
+  let val _ = Output.debug (fn()=>"  abstraction: " ^ Display.string_of_cterm ct)
       val Abs(x,_,body) = term_of ct
       val thy = theory_of_cterm ct
       val Type("fun",[xT,bodyT]) = typ_of (ctyp_of_term ct)
       val cxT = ctyp_of thy xT and cbodyT = ctyp_of thy bodyT
       fun makeK() = instantiate' [SOME cxT, SOME cbodyT] [SOME (cterm_of thy body)] abs_K

   else
   case term_of ct of
       Abs _ =>
 	let val (cv,cta) = Thm.dest_abs NONE ct
 	    val (v,Tv) = (dest_Free o term_of) cv
-	    val _ = Output.debug (fn()=>"  recursion: " ^ string_of_cterm cta);
+	    val _ = Output.debug (fn()=>"  recursion: " ^ Display.string_of_cterm cta);
 	    val u_th = combinators_aux cta
-	    val _ = Output.debug (fn()=>"  returned " ^ string_of_thm u_th);
+	    val _ = Output.debug (fn()=>"  returned " ^ Display.string_of_thm u_th);
 	    val cu = Thm.rhs_of u_th
 	    val comb_eq = abstract (Thm.cabs cv cu)
-	in Output.debug (fn()=>"  abstraction result: " ^ string_of_thm comb_eq);
+	in Output.debug (fn()=>"  abstraction result: " ^ Display.string_of_thm comb_eq);
 	   (transitive (abstract_rule v cv u_th) comb_eq) end
     | t1 $ t2 =>
 	let val (ct1,ct2) = Thm.dest_comb ct
 	in  combination (combinators_aux ct1) (combinators_aux ct2)  end;
             
 fun combinators th =
   if lambda_free (prop_of th) then th 
   else
-    let val _ = Output.debug (fn()=>"Conversion to combinators: " ^ string_of_thm th);
+    let val _ = Output.debug (fn()=>"Conversion to combinators: " ^ Display.string_of_thm th);
 	val th = Drule.eta_contraction_rule th
 	val eqth = combinators_aux (cprop_of th)
-	val _ = Output.debug (fn()=>"Conversion result: " ^ string_of_thm eqth);
+	val _ = Output.debug (fn()=>"Conversion result: " ^ Display.string_of_thm eqth);
     in  equal_elim eqth th   end
     handle THM (msg,_,_) => 
-      (warning ("Error in the combinator translation of " ^ string_of_thm th);
+      (warning ("Error in the combinator translation of " ^ Display.string_of_thm th);
        warning ("  Exception message: " ^ msg);
        TrueI);  (*A type variable of sort {} will cause make abstraction fail.*)
 
 (*cterms are used throughout for efficiency*)
 val cTrueprop = Thm.cterm_of HOL.thy HOLogic.Trueprop;

   map (skolem_of_def o assume o (cterm_of (theory_of_thm th))) (assume_skofuns s th);
 
 fun assert_lambda_free ths msg =
   case filter (not o lambda_free o prop_of) ths of
       [] => ()
-    | ths' => error (msg ^ "\n" ^ cat_lines (map string_of_thm ths'));
+    | ths' => error (msg ^ "\n" ^ cat_lines (map Display.string_of_thm ths'));
 
 
 (*** Blacklisting (duplicated in ResAtp? ***)
 
 val max_lambda_nesting = 3;

   if PureThy.has_name_hint th then flatten_name (PureThy.get_name_hint th)
   else gensym "unknown_thm_";
 
 fun name_or_string th =
   if PureThy.has_name_hint th then PureThy.get_name_hint th
-  else string_of_thm th;
+  else Display.string_of_thm th;
 
 (*Declare Skolem functions for a theorem, supplied in nnf and with its name.
   It returns a modified theory, unless skolemization fails.*)
 fun skolem thy th =
   let val ctxt0 = Variable.thm_context th
       val _ = Output.debug (fn () => "skolemizing " ^ name_or_string th)
   in
      Option.map
         (fn (nnfth,ctxt1) =>
           let 
-              val _ = Output.debug (fn () => "  initial nnf: " ^ string_of_thm nnfth)
+              val _ = Output.debug (fn () => "  initial nnf: " ^ Display.string_of_thm nnfth)
               val s = fake_name th
               val (thy',defs) = declare_skofuns s nnfth thy
               val (cnfs,ctxt2) = Meson.make_cnf (map skolem_of_def defs) nnfth ctxt1
               val _ = Output.debug (fn () => Int.toString (length cnfs) ^ " clauses yielded")
               val cnfs' = cnfs |> map combinators |> Variable.export ctxt2 ctxt0 

       val defs = filter (is_absko o Thm.term_of) newhyps
       val remaining_hyps = filter_out (member (op aconv) (map Thm.term_of defs))
                                       (map Thm.term_of hyps)
       val fixed = term_frees (concl_of st) @
                   foldl (gen_union (op aconv)) [] (map term_frees remaining_hyps)
-  in  Output.debug (fn _ => "expand_defs_tac: " ^ string_of_thm st);
-      Output.debug (fn _ => "  st0: " ^ string_of_thm st0);
-      Output.debug (fn _ => "  defs: " ^ commas (map string_of_cterm defs));
+  in  Output.debug (fn _ => "expand_defs_tac: " ^ Display.string_of_thm st);
+      Output.debug (fn _ => "  st0: " ^ Display.string_of_thm st0);
+      Output.debug (fn _ => "  defs: " ^ commas (map Display.string_of_cterm defs));
       Seq.of_list [LocalDefs.expand (filter (is_okdef fixed o Thm.term_of) defs) st]
   end;
 
 
 fun meson_general_tac ths i st0 =
- let val _ = Output.debug (fn () => "Meson called: " ^ cat_lines (map string_of_thm ths))
+ let val _ = Output.debug (fn () => "Meson called: " ^ cat_lines (map Display.string_of_thm ths))
  in  (Meson.meson_claset_tac (cnf_rules_of_ths ths) HOL_cs i THEN expand_defs_tac st0) st0 end;
 
 val meson_method_setup = Method.add_methods
   [("meson", Method.thms_args (fn ths =>
       Method.SIMPLE_METHOD' (CHANGED_PROP o meson_general_tac ths)),