structure Display: less pervasive operations;
authorwenzelm
Sat May 17 13:54:30 2008 +0200 (2008-05-17)
changeset 26928ca87aff1ad2d
parent 26927 8684b5240f11
child 26929 bad4e1819b42
structure Display: less pervasive operations;
src/FOLP/classical.ML
src/FOLP/simp.ML
src/HOL/Import/hol4rews.ML
src/HOL/Import/import_package.ML
src/HOL/Import/proof_kernel.ML
src/HOL/Import/shuffler.ML
src/HOL/Nominal/nominal_thmdecls.ML
src/HOL/Tools/Qelim/cooper.ML
src/HOL/Tools/TFL/rules.ML
src/HOL/Tools/TFL/tfl.ML
src/HOL/Tools/inductive_codegen.ML
src/HOL/Tools/inductive_package.ML
src/HOL/Tools/inductive_realizer.ML
src/HOL/Tools/meson.ML
src/HOL/Tools/metis_tools.ML
src/HOL/Tools/recfun_codegen.ML
src/HOL/Tools/res_atp.ML
src/HOL/Tools/res_axioms.ML
src/HOL/Tools/res_reconstruct.ML
src/HOL/Tools/sat_funcs.ML
src/HOL/Tools/specification_package.ML
src/HOL/Tools/watcher.ML
src/Provers/blast.ML
src/Provers/classical.ML
src/Pure/Isar/code.ML
src/Pure/display.ML
src/Pure/old_goals.ML
src/Sequents/prover.ML
src/Sequents/simpdata.ML
src/Tools/code/code_funcgr.ML
src/ZF/Datatype_ZF.thy
src/ZF/Tools/inductive_package.ML
     1.1 --- a/src/FOLP/classical.ML	Fri May 16 23:25:37 2008 +0200
     1.2 +++ b/src/FOLP/classical.ML	Sat May 17 13:54:30 2008 +0200
     1.3 @@ -124,10 +124,10 @@
     1.4  val empty_cs = make_cs{safeIs=[], safeEs=[], hazIs=[], hazEs=[]};
     1.5  
     1.6  fun print_cs (CS{safeIs,safeEs,hazIs,hazEs,...}) =
     1.7 - (writeln"Introduction rules";  prths hazIs;
     1.8 -  writeln"Safe introduction rules";  prths safeIs;
     1.9 -  writeln"Elimination rules";  prths hazEs;
    1.10 -  writeln"Safe elimination rules";  prths safeEs;
    1.11 + (writeln"Introduction rules";  Display.prths hazIs;
    1.12 +  writeln"Safe introduction rules";  Display.prths safeIs;
    1.13 +  writeln"Elimination rules";  Display.prths hazEs;
    1.14 +  writeln"Safe elimination rules";  Display.prths safeEs;
    1.15    ());
    1.16  
    1.17  fun (CS{safeIs,safeEs,hazIs,hazEs,...}) addSIs ths =
     2.1 --- a/src/FOLP/simp.ML	Fri May 16 23:25:37 2008 +0200
     2.2 +++ b/src/FOLP/simp.ML	Sat May 17 13:54:30 2008 +0200
     2.3 @@ -114,7 +114,7 @@
     2.4    let fun norm thm = 
     2.5        case lhs_of(concl_of thm) of
     2.6            Const(n,_)$_ => n
     2.7 -        | _ => (prths normE_thms; error"No constant in lhs of a norm_thm")
     2.8 +        | _ => (Display.prths normE_thms; error"No constant in lhs of a norm_thm")
     2.9    in map norm normE_thms end;
    2.10  
    2.11  fun lhs_is_NORM(thm,i) = case lhs_of_eq i thm of
    2.12 @@ -123,7 +123,7 @@
    2.13  val refl_tac = resolve_tac refl_thms;
    2.14  
    2.15  fun find_res thms thm =
    2.16 -    let fun find [] = (prths thms; error"Check Simp_Data")
    2.17 +    let fun find [] = (Display.prths thms; error"Check Simp_Data")
    2.18            | find(th::thms) = thm RS th handle THM _ => find thms
    2.19      in find thms end;
    2.20  
    2.21 @@ -250,7 +250,7 @@
    2.22  fun insert_thm_warn th net = 
    2.23    Net.insert_term Thm.eq_thm_prop (concl_of th, th) net
    2.24    handle Net.INSERT => 
    2.25 -    (writeln"\nDuplicate rewrite or congruence rule:"; print_thm th;
    2.26 +    (writeln"\nDuplicate rewrite or congruence rule:"; Display.print_thm th;
    2.27       net);
    2.28  
    2.29  val insert_thms = fold_rev insert_thm_warn;
    2.30 @@ -276,7 +276,7 @@
    2.31  fun delete_thm_warn th net = 
    2.32    Net.delete_term Thm.eq_thm_prop (concl_of th, th) net
    2.33    handle Net.DELETE => 
    2.34 -    (writeln"\nNo such rewrite or congruence rule:";  print_thm th;
    2.35 +    (writeln"\nNo such rewrite or congruence rule:";  Display.print_thm th;
    2.36       net);
    2.37  
    2.38  val delete_thms = fold_rev delete_thm_warn;
    2.39 @@ -292,7 +292,7 @@
    2.40  let fun find((p as (th,ths))::ps',ps) =
    2.41            if Thm.eq_thm_prop(thm,th) then (ths,ps@ps') else find(ps',p::ps)
    2.42        | find([],simps') = (writeln"\nNo such rewrite or congruence rule:";
    2.43 -                           print_thm thm;
    2.44 +                           Display.print_thm thm;
    2.45                             ([],simps'))
    2.46      val (thms,simps') = find(simps,[])
    2.47  in SS{auto_tac=auto_tac, congs=congs, cong_net=cong_net, mk_simps=mk_simps,
    2.48 @@ -312,8 +312,8 @@
    2.49  fun dest_ss(SS{congs,simps,...}) = (congs, map #1 simps);
    2.50  
    2.51  fun print_ss(SS{congs,simps,...}) =
    2.52 -        (writeln"Congruences:"; prths congs;
    2.53 -         writeln"Rewrite Rules:"; prths (map #1 simps); ());
    2.54 +        (writeln"Congruences:"; Display.prths congs;
    2.55 +         writeln"Rewrite Rules:"; Display.prths (map #1 simps); ());
    2.56  
    2.57  
    2.58  (* Rewriting with conditionals *)
    2.59 @@ -436,7 +436,7 @@
    2.60          val rwrls = map mk_trans (List.concat(map mk_rew_rules thms));
    2.61          val anet' = foldr lhs_insert_thm anet rwrls
    2.62      in  if !tracing andalso not(null new_rws)
    2.63 -        then (writeln"Adding rewrites:";  prths new_rws;  ())
    2.64 +        then (writeln"Adding rewrites:";  Display.prths new_rws;  ())
    2.65          else ();
    2.66          (ss,thm,anet',anet::ats,cs) 
    2.67      end;
     3.1 --- a/src/HOL/Import/hol4rews.ML	Fri May 16 23:25:37 2008 +0200
     3.2 +++ b/src/HOL/Import/hol4rews.ML	Sat May 17 13:54:30 2008 +0200
     3.3 @@ -532,7 +532,7 @@
     3.4  	val _ = app (fn (hol,(internal,isa,opt_ty)) =>
     3.5  			(out ("\n  " ^ (trans_string hol) ^ " > " ^ (trans_string (follow_cname isa thy)));
     3.6  			 case opt_ty of
     3.7 -			     SOME ty => out (" :: \"" ^ (string_of_ctyp (ctyp_of thy ty)) ^ "\"")
     3.8 +			     SOME ty => out (" :: \"" ^ (Display.string_of_ctyp (ctyp_of thy ty)) ^ "\"")
     3.9  			   | NONE => ())) constmaps
    3.10  	val _ = if null constmaps
    3.11  		then ()
     4.1 --- a/src/HOL/Import/import_package.ML	Fri May 16 23:25:37 2008 +0200
     4.2 +++ b/src/HOL/Import/import_package.ML	Sat May 17 13:54:30 2008 +0200
     4.3 @@ -25,8 +25,8 @@
     4.4  val debug = ref false
     4.5  fun message s = if !debug then writeln s else ()
     4.6  
     4.7 -val string_of_thm = PrintMode.setmp [] string_of_thm;
     4.8 -val string_of_cterm = PrintMode.setmp [] string_of_cterm;
     4.9 +val string_of_thm = PrintMode.setmp [] Display.string_of_thm;
    4.10 +val string_of_cterm = PrintMode.setmp [] Display.string_of_cterm;
    4.11  
    4.12  fun import_tac (thyname,thmname) =
    4.13      if ! quick_and_dirty
     5.1 --- a/src/HOL/Import/proof_kernel.ML	Fri May 16 23:25:37 2008 +0200
     5.2 +++ b/src/HOL/Import/proof_kernel.ML	Sat May 17 13:54:30 2008 +0200
     5.3 @@ -205,7 +205,7 @@
     5.4          Library.setmp show_brackets false (
     5.5          Library.setmp show_all_types true (
     5.6          Library.setmp Syntax.ambiguity_is_error false (
     5.7 -        Library.setmp show_sorts true string_of_cterm))))
     5.8 +        Library.setmp show_sorts true Display.string_of_cterm))))
     5.9          ct)
    5.10      end
    5.11  
    5.12 @@ -227,7 +227,7 @@
    5.13            | G _ = raise SMART_STRING
    5.14          fun F n =
    5.15              let
    5.16 -                val str = Library.setmp show_brackets false (G n string_of_cterm) ct
    5.17 +                val str = Library.setmp show_brackets false (G n Display.string_of_cterm) ct
    5.18                  val u = Syntax.parse_term ctxt str
    5.19                    |> TypeInfer.constrain T |> Syntax.check_term ctxt
    5.20              in
    5.21 @@ -236,7 +236,7 @@
    5.22                  else F (n+1)
    5.23              end
    5.24              handle ERROR mesg => F (n+1)
    5.25 -                 | SMART_STRING => raise ERROR ("smart_string failed for: "^(G 0 string_of_cterm ct))
    5.26 +                 | SMART_STRING => raise ERROR ("smart_string failed for: "^(G 0 Display.string_of_cterm ct))
    5.27      in
    5.28        PrintMode.setmp [] (Library.setmp Syntax.ambiguity_is_error true F) 0
    5.29      end
    5.30 @@ -244,8 +244,8 @@
    5.31  
    5.32  val smart_string_of_thm = smart_string_of_cterm o cprop_of
    5.33  
    5.34 -fun prth th = writeln (PrintMode.setmp [] string_of_thm th)
    5.35 -fun prc ct = writeln (PrintMode.setmp [] string_of_cterm ct)
    5.36 +fun prth th = writeln (PrintMode.setmp [] Display.string_of_thm th)
    5.37 +fun prc ct = writeln (PrintMode.setmp [] Display.string_of_cterm ct)
    5.38  fun prin t = writeln (PrintMode.setmp [] (fn () => Sign.string_of_term (the_context ()) t) ());
    5.39  fun pth (HOLThm(ren,thm)) =
    5.40      let
    5.41 @@ -1947,14 +1947,14 @@
    5.42                      then
    5.43                          let
    5.44                              val p1 = quotename constname
    5.45 -                            val p2 = string_of_ctyp (ctyp_of thy'' ctype)
    5.46 +                            val p2 = Display.string_of_ctyp (ctyp_of thy'' ctype)
    5.47                              val p3 = string_of_mixfix csyn
    5.48                              val p4 = smart_string_of_cterm crhs
    5.49                          in
    5.50                              add_dump ("constdefs\n  " ^p1^ " :: \"" ^p2^ "\" "^p3^ "\n  " ^p4) thy''
    5.51                          end
    5.52                      else
    5.53 -                        (add_dump ("consts\n  " ^ (quotename constname) ^ " :: \"" ^ string_of_ctyp (ctyp_of thy'' ctype) ^
    5.54 +                        (add_dump ("consts\n  " ^ (quotename constname) ^ " :: \"" ^ Display.string_of_ctyp (ctyp_of thy'' ctype) ^
    5.55                                     "\" " ^ (string_of_mixfix csyn) ^ "\n\ndefs\n  " ^ (quotename thmname) ^ ": " ^ (smart_string_of_cterm crhs))
    5.56                                    thy'')
    5.57          val hth = case Shuffler.set_prop thy22 (HOLogic.mk_Trueprop tm24) [("",th)] of
    5.58 @@ -2017,7 +2017,7 @@
    5.59                                                                ((cname,cT,mk_syn thy cname)::cs,p)
    5.60                                                            end) (([],HOLogic.dest_Trueprop (concl_of th)),names)
    5.61                                 val str = Library.foldl (fn (acc,(c,T,csyn)) =>
    5.62 -                                                   acc ^ "\n  " ^ (quotename c) ^ " :: \"" ^ string_of_ctyp (ctyp_of thy T) ^ "\" " ^ (string_of_mixfix csyn)) ("consts",consts)
    5.63 +                                                   acc ^ "\n  " ^ (quotename c) ^ " :: \"" ^ Display.string_of_ctyp (ctyp_of thy T) ^ "\" " ^ (string_of_mixfix csyn)) ("consts",consts)
    5.64                                 val thy' = add_dump str thy
    5.65                                 val _ = ImportRecorder.add_consts consts
    5.66                             in
    5.67 @@ -2143,7 +2143,7 @@
    5.68  fun add_dump_constdefs thy defname constname rhs ty =
    5.69      let
    5.70          val n = quotename constname
    5.71 -        val t = string_of_ctyp (ctyp_of thy ty)
    5.72 +        val t = Display.string_of_ctyp (ctyp_of thy ty)
    5.73          val syn = string_of_mixfix (mk_syn thy constname)
    5.74          (*val eq = smart_string_of_cterm (cterm_of thy (Const(rhs, ty)))*)
    5.75          val eq = quote (constname ^ " == "^rhs)
    5.76 @@ -2228,7 +2228,7 @@
    5.77                ("  apply (rule light_ex_imp_nonempty[where t="^
    5.78                (proc_prop (cterm_of thy4 t))^"])\n"^
    5.79                ("  by (import " ^ thyname ^ " " ^ (quotename thmname) ^ ")"))) thy4
    5.80 -            val str_aty = string_of_ctyp (ctyp_of thy aty)
    5.81 +            val str_aty = Display.string_of_ctyp (ctyp_of thy aty)
    5.82              val thy = add_dump_syntax thy rep_name
    5.83              val thy = add_dump_syntax thy abs_name
    5.84              val thy = add_dump ("lemmas " ^ (quote (thmname^"_@intern")) ^
     6.1 --- a/src/HOL/Import/shuffler.ML	Fri May 16 23:25:37 2008 +0200
     6.2 +++ b/src/HOL/Import/shuffler.ML	Sat May 17 13:54:30 2008 +0200
     6.3 @@ -42,7 +42,7 @@
     6.4    case e of
     6.5       THM (msg,i,thms) =>
     6.6           (writeln ("Exception THM " ^ string_of_int i ^ " raised:\n" ^ msg);
     6.7 -          List.app print_thm thms)
     6.8 +          List.app Display.print_thm thms)
     6.9     | THEORY (msg,thys) =>
    6.10           (writeln ("Exception THEORY raised:\n" ^ msg);
    6.11            List.app (writeln o Context.str_of_thy) thys)
    6.12 @@ -58,8 +58,8 @@
    6.13  (*Prints an exception, then fails*)
    6.14  fun print_sign_exn sign e = (print_sign_exn_unit sign e; raise e)
    6.15  
    6.16 -val string_of_thm = PrintMode.setmp [] string_of_thm;
    6.17 -val string_of_cterm = PrintMode.setmp [] string_of_cterm;
    6.18 +val string_of_thm = PrintMode.setmp [] Display.string_of_thm;
    6.19 +val string_of_cterm = PrintMode.setmp [] Display.string_of_cterm;
    6.20  
    6.21  fun mk_meta_eq th =
    6.22      (case concl_of th of
    6.23 @@ -305,11 +305,11 @@
    6.24              in
    6.25                  if not (lhs aconv origt)
    6.26                  then (writeln "Something is utterly wrong: (orig,lhs,frozen type,t,tinst)";
    6.27 -                      writeln (string_of_cterm (cterm_of thy origt));
    6.28 -                      writeln (string_of_cterm (cterm_of thy lhs));
    6.29 -                      writeln (string_of_cterm (cterm_of thy typet));
    6.30 -                      writeln (string_of_cterm (cterm_of thy t));
    6.31 -                      app (fn (n,T) => writeln (n ^ ": " ^ (string_of_ctyp (ctyp_of thy T)))) Tinst;
    6.32 +                      writeln (Display.string_of_cterm (cterm_of thy origt));
    6.33 +                      writeln (Display.string_of_cterm (cterm_of thy lhs));
    6.34 +                      writeln (Display.string_of_cterm (cterm_of thy typet));
    6.35 +                      writeln (Display.string_of_cterm (cterm_of thy t));
    6.36 +                      app (fn (n,T) => writeln (n ^ ": " ^ (Display.string_of_ctyp (ctyp_of thy T)))) Tinst;
    6.37                        writeln "done")
    6.38                  else ()
    6.39              end
    6.40 @@ -367,11 +367,11 @@
    6.41              in
    6.42                  if not (lhs aconv origt)
    6.43                  then (writeln "Something is utterly wrong: (orig,lhs,frozen type,t,tinst)";
    6.44 -                      writeln (string_of_cterm (cterm_of thy origt));
    6.45 -                      writeln (string_of_cterm (cterm_of thy lhs));
    6.46 -                      writeln (string_of_cterm (cterm_of thy typet));
    6.47 -                      writeln (string_of_cterm (cterm_of thy t));
    6.48 -                      app (fn (n,T) => writeln (n ^ ": " ^ (string_of_ctyp (ctyp_of thy T)))) Tinst;
    6.49 +                      writeln (Display.string_of_cterm (cterm_of thy origt));
    6.50 +                      writeln (Display.string_of_cterm (cterm_of thy lhs));
    6.51 +                      writeln (Display.string_of_cterm (cterm_of thy typet));
    6.52 +                      writeln (Display.string_of_cterm (cterm_of thy t));
    6.53 +                      app (fn (n,T) => writeln (n ^ ": " ^ (Display.string_of_ctyp (ctyp_of thy T)))) Tinst;
    6.54                        writeln "done")
    6.55                  else ()
    6.56              end
     7.1 --- a/src/HOL/Nominal/nominal_thmdecls.ML	Fri May 16 23:25:37 2008 +0200
     7.2 +++ b/src/HOL/Nominal/nominal_thmdecls.ML	Sat May 17 13:54:30 2008 +0200
     7.3 @@ -159,7 +159,7 @@
     7.4        fold (fn thm => Data.map (flag thm)) thms_to_be_added context
     7.5    end
     7.6    handle EQVT_FORM s =>
     7.7 -      error (string_of_thm orig_thm ^ " does not comply with the form of an equivariance lemma ("^s^").")
     7.8 +      error (Display.string_of_thm orig_thm ^ " does not comply with the form of an equivariance lemma ("^s^").")
     7.9  
    7.10  (* in cases of bij- and freshness, we just add the lemmas to the *)
    7.11  (* data-slot *)
     8.1 --- a/src/HOL/Tools/Qelim/cooper.ML	Fri May 16 23:25:37 2008 +0200
     8.2 +++ b/src/HOL/Tools/Qelim/cooper.ML	Sat May 17 13:54:30 2008 +0200
     8.3 @@ -324,7 +324,7 @@
     8.4              in 
     8.5               (fn ct => (valOf (Inttab.lookup tab (ct |> term_of |> dest_numeral)) 
     8.6                  handle Option => (writeln "noz: Theorems-Table contains no entry for"; 
     8.7 -                                    print_cterm ct ; raise Option)))
     8.8 +                                    Display.print_cterm ct ; raise Option)))
     8.9             end
    8.10    fun unit_conv t = 
    8.11     case (term_of t) of
    8.12 @@ -414,7 +414,7 @@
    8.13                                 (ds ~~ (map divprop ds)) Inttab.empty in 
    8.14             (fn ct => (valOf (Inttab.lookup tab (term_of ct |> dest_numeral)) 
    8.15                      handle Option => (writeln "dvd: Theorems-Table contains no entry for"; 
    8.16 -                                      print_cterm ct ; raise Option)))
    8.17 +                                      Display.print_cterm ct ; raise Option)))
    8.18             end
    8.19   val dp = 
    8.20     let val th = Simplifier.rewrite lin_ss 
    8.21 @@ -485,7 +485,7 @@
    8.22                    sths) Termtab.empty
    8.23          in fn ct => 
    8.24            (valOf (Termtab.lookup tab (term_of ct))
    8.25 -           handle Option => (writeln "inS: No theorem for " ; print_cterm ct ; raise Option))
    8.26 +           handle Option => (writeln "inS: No theorem for " ; Display.print_cterm ct ; raise Option))
    8.27          end
    8.28         val (inf, nb, pd) = divide_and_conquer (f x dvd inS (abths S)) p
    8.29     in [dp, inf, nb, pd] MRS cpth
     9.1 --- a/src/HOL/Tools/TFL/rules.ML	Fri May 16 23:25:37 2008 +0200
     9.2 +++ b/src/HOL/Tools/TFL/rules.ML	Sat May 17 13:54:30 2008 +0200
     9.3 @@ -554,10 +554,10 @@
     9.4  fun say s = if !tracing then writeln s else ();
     9.5  
     9.6  fun print_thms s L =
     9.7 -  say (cat_lines (s :: map string_of_thm L));
     9.8 +  say (cat_lines (s :: map Display.string_of_thm L));
     9.9  
    9.10  fun print_cterms s L =
    9.11 -  say (cat_lines (s :: map string_of_cterm L));
    9.12 +  say (cat_lines (s :: map Display.string_of_cterm L));
    9.13  
    9.14  
    9.15  (*---------------------------------------------------------------------------
    9.16 @@ -679,7 +679,7 @@
    9.17               val cntxt = MetaSimplifier.prems_of_ss ss
    9.18               val dummy = print_thms "cntxt:" cntxt
    9.19               val dummy = say "cong rule:"
    9.20 -             val dummy = say (string_of_thm thm)
    9.21 +             val dummy = say (Display.string_of_thm thm)
    9.22               val dummy = thm_ref := (thm :: !thm_ref)
    9.23               val dummy = ss_ref := (ss :: !ss_ref)
    9.24               (* Unquantified eliminate *)
    10.1 --- a/src/HOL/Tools/TFL/tfl.ML	Fri May 16 23:25:37 2008 +0200
    10.2 +++ b/src/HOL/Tools/TFL/tfl.ML	Sat May 17 13:54:30 2008 +0200
    10.3 @@ -298,7 +298,7 @@
    10.4              raise TFL_ERR "no_repeat_vars"
    10.5                            (quote (#1 (dest_Free v)) ^
    10.6                            " occurs repeatedly in the pattern " ^
    10.7 -                          quote (string_of_cterm (Thry.typecheck thy pat)))
    10.8 +                          quote (Display.string_of_cterm (Thry.typecheck thy pat)))
    10.9           else check rst
   10.10   in check (FV_multiset pat)
   10.11   end;
   10.12 @@ -532,7 +532,7 @@
   10.13       val (extractants,TCl) = ListPair.unzip extracta
   10.14       val dummy = if !trace
   10.15                   then (writeln "Extractants = ";
   10.16 -                       prths extractants;
   10.17 +                       Display.prths extractants;
   10.18                         ())
   10.19                   else ()
   10.20       val TCs = foldr (gen_union (op aconv)) [] TCl
   10.21 @@ -553,7 +553,7 @@
   10.22         |> PureThy.add_defs_i false
   10.23              [Thm.no_attributes (fid ^ "_def", defn)]
   10.24       val def = Thm.freezeT def0;
   10.25 -     val dummy = if !trace then writeln ("DEF = " ^ string_of_thm def)
   10.26 +     val dummy = if !trace then writeln ("DEF = " ^ Display.string_of_thm def)
   10.27                             else ()
   10.28       (* val fconst = #lhs(S.dest_eq(concl def))  *)
   10.29       val tych = Thry.typecheck theory
   10.30 @@ -562,7 +562,7 @@
   10.31       val baz = R.DISCH_ALL
   10.32                   (fold_rev R.DISCH full_rqt_prop
   10.33                    (R.LIST_CONJ extractants))
   10.34 -     val dum = if !trace then writeln ("baz = " ^ string_of_thm baz)
   10.35 +     val dum = if !trace then writeln ("baz = " ^ Display.string_of_thm baz)
   10.36                             else ()
   10.37       val f_free = Free (fid, fastype_of f)  (*'cos f is a Const*)
   10.38       val SV' = map tych SV;
   10.39 @@ -911,11 +911,11 @@
   10.40  
   10.41  
   10.42  fun trace_thms s L =
   10.43 -  if !trace then writeln (cat_lines (s :: map string_of_thm L))
   10.44 +  if !trace then writeln (cat_lines (s :: map Display.string_of_thm L))
   10.45    else ();
   10.46  
   10.47  fun trace_cterms s L =
   10.48 -  if !trace then writeln (cat_lines (s :: map string_of_cterm L))
   10.49 +  if !trace then writeln (cat_lines (s :: map Display.string_of_cterm L))
   10.50    else ();;
   10.51  
   10.52  
    11.1 --- a/src/HOL/Tools/inductive_codegen.ML	Fri May 16 23:25:37 2008 +0200
    11.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Sat May 17 13:54:30 2008 +0200
    11.3 @@ -40,7 +40,7 @@
    11.4  
    11.5  
    11.6  fun warn thm = warning ("InductiveCodegen: Not a proper clause:\n" ^
    11.7 -  string_of_thm thm);
    11.8 +  Display.string_of_thm thm);
    11.9  
   11.10  fun add_node (g, x) = Graph.new_node (x, ()) g handle Graph.DUP _ => g;
   11.11  
    12.1 --- a/src/HOL/Tools/inductive_package.ML	Fri May 16 23:25:37 2008 +0200
    12.2 +++ b/src/HOL/Tools/inductive_package.ML	Sat May 17 13:54:30 2008 +0200
    12.3 @@ -180,7 +180,7 @@
    12.4        [dest_less_concl (Seq.hd (REPEAT (FIRSTGOAL
    12.5           (resolve_tac [le_funI, le_boolI'])) thm))]
    12.6      | _ => [thm]
    12.7 -  end handle THM _ => error ("Bad monotonicity theorem:\n" ^ string_of_thm thm);
    12.8 +  end handle THM _ => error ("Bad monotonicity theorem:\n" ^ Display.string_of_thm thm);
    12.9  
   12.10  val mono_add = Thm.declaration_attribute (map_monos o fold Thm.add_thm o mk_mono);
   12.11  val mono_del = Thm.declaration_attribute (map_monos o fold Thm.del_thm o mk_mono);
    13.1 --- a/src/HOL/Tools/inductive_realizer.ML	Fri May 16 23:25:37 2008 +0200
    13.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Sat May 17 13:54:30 2008 +0200
    13.3 @@ -19,7 +19,7 @@
    13.4  fun name_of_thm thm =
    13.5    (case Symtab.dest (Proofterm.thms_of_proof' (proof_of thm) Symtab.empty) of
    13.6       [(name, _)] => name
    13.7 -   | _ => error ("name_of_thm: bad proof of theorem\n" ^ string_of_thm thm));
    13.8 +   | _ => error ("name_of_thm: bad proof of theorem\n" ^ Display.string_of_thm thm));
    13.9  
   13.10  val all_simps = map (symmetric o mk_meta_eq) (thms "HOL.all_simps");
   13.11  
    14.1 --- a/src/HOL/Tools/meson.ML	Fri May 16 23:25:37 2008 +0200
    14.2 +++ b/src/HOL/Tools/meson.ML	Sat May 17 13:54:30 2008 +0200
    14.3 @@ -121,9 +121,9 @@
    14.4    let fun forward_tacf [prem] = rtac (nf prem) 1
    14.5          | forward_tacf prems =
    14.6              error ("Bad proof state in forward_res, please inform lcp@cl.cam.ac.uk:\n" ^
    14.7 -                   string_of_thm st ^
    14.8 +                   Display.string_of_thm st ^
    14.9                     "\nPremises:\n" ^
   14.10 -                   cat_lines (map string_of_thm prems))
   14.11 +                   cat_lines (map Display.string_of_thm prems))
   14.12    in
   14.13      case Seq.pull (ALLGOALS (METAHYPS forward_tacf) st)
   14.14      of SOME(th,_) => th
   14.15 @@ -335,7 +335,7 @@
   14.16        and cnf_nil th = cnf_aux (th,[])
   14.17        val cls = 
   14.18  	    if too_many_clauses (SOME ctxt) (concl_of th)
   14.19 -	    then (warning ("cnf is ignoring: " ^ string_of_thm th); ths)
   14.20 +	    then (warning ("cnf is ignoring: " ^ Display.string_of_thm th); ths)
   14.21  	    else cnf_aux (th,ths)
   14.22    in  (cls, !ctxtr)  end;
   14.23  
   14.24 @@ -535,7 +535,7 @@
   14.25    | skolemize_nnf_list (th::ths) = 
   14.26        skolemize (make_nnf th) :: skolemize_nnf_list ths
   14.27        handle THM _ => (*RS can fail if Unify.search_bound is too small*)
   14.28 -       (warning ("Failed to Skolemize " ^ string_of_thm th);
   14.29 +       (warning ("Failed to Skolemize " ^ Display.string_of_thm th);
   14.30          skolemize_nnf_list ths);
   14.31  
   14.32  fun add_clauses (th,cls) =
   14.33 @@ -625,9 +625,9 @@
   14.34               let val horns = make_horns (cls@ths)
   14.35                   val _ =
   14.36                       Output.debug (fn () => ("meson method called:\n" ^
   14.37 -                                  space_implode "\n" (map string_of_thm (cls@ths)) ^
   14.38 +                                  space_implode "\n" (map Display.string_of_thm (cls@ths)) ^
   14.39                                    "\nclauses:\n" ^
   14.40 -                                  space_implode "\n" (map string_of_thm horns)))
   14.41 +                                  space_implode "\n" (map Display.string_of_thm horns)))
   14.42               in THEN_ITER_DEEPEN (resolve_tac goes 1) (has_fewer_prems 1) (prolog_step_tac' horns)
   14.43               end
   14.44   );
    15.1 --- a/src/HOL/Tools/metis_tools.ML	Fri May 16 23:25:37 2008 +0200
    15.2 +++ b/src/HOL/Tools/metis_tools.ML	Sat May 17 13:54:30 2008 +0200
    15.3 @@ -270,7 +270,7 @@
    15.4    fun print_thpair (fth,th) =
    15.5      (Output.debug (fn () => "=============================================");
    15.6       Output.debug (fn () => "Metis: " ^ Metis.Thm.toString fth);
    15.7 -     Output.debug (fn () => "Isabelle: " ^ string_of_thm th));
    15.8 +     Output.debug (fn () => "Isabelle: " ^ Display.string_of_thm th));
    15.9  
   15.10    fun lookth thpairs (fth : Metis.Thm.thm) =
   15.11      valOf (AList.lookup (uncurry Metis.Thm.equal) thpairs fth)
   15.12 @@ -309,7 +309,7 @@
   15.13                in  SOME (cterm_of thy v, t)  end
   15.14                handle Option =>
   15.15                    (Output.debug (fn() => "List.find failed for the variable " ^ x ^
   15.16 -                                         " in " ^ string_of_thm i_th);
   15.17 +                                         " in " ^ Display.string_of_thm i_th);
   15.18                     NONE)
   15.19          fun remove_typeinst (a, t) =
   15.20                case Recon.strip_prefix ResClause.schematic_var_prefix a of
   15.21 @@ -317,15 +317,15 @@
   15.22                  | NONE   => case Recon.strip_prefix ResClause.tvar_prefix a of
   15.23                    SOME _ => NONE          (*type instantiations are forbidden!*)
   15.24                  | NONE   => SOME (a,t)    (*internal Metis var?*)
   15.25 -        val _ = Output.debug (fn () => "  isa th: " ^ string_of_thm i_th)
   15.26 +        val _ = Output.debug (fn () => "  isa th: " ^ Display.string_of_thm i_th)
   15.27          val substs = List.mapPartial remove_typeinst (Metis.Subst.toList fsubst)
   15.28          val (vars,rawtms) = ListPair.unzip (List.mapPartial subst_translation substs)
   15.29          val tms = infer_types ctxt rawtms;
   15.30          val ctm_of = cterm_incr_types thy (1 + Thm.maxidx_of i_th)
   15.31          val substs' = ListPair.zip (vars, map ctm_of tms)
   15.32          val _ = Output.debug (fn() => "subst_translations:")
   15.33 -        val _ = app (fn (x,y) => Output.debug (fn () => string_of_cterm x ^ " |-> " ^
   15.34 -                                                        string_of_cterm y))
   15.35 +        val _ = app (fn (x,y) => Output.debug (fn () => Display.string_of_cterm x ^ " |-> " ^
   15.36 +                                                        Display.string_of_cterm y))
   15.37                    substs'
   15.38      in  cterm_instantiate substs' i_th  end;
   15.39  
   15.40 @@ -347,8 +347,8 @@
   15.41      let
   15.42        val thy = ProofContext.theory_of ctxt
   15.43        val i_th1 = lookth thpairs th1 and i_th2 = lookth thpairs th2
   15.44 -      val _ = Output.debug (fn () => "  isa th1 (pos): " ^ string_of_thm i_th1)
   15.45 -      val _ = Output.debug (fn () => "  isa th2 (neg): " ^ string_of_thm i_th2)
   15.46 +      val _ = Output.debug (fn () => "  isa th1 (pos): " ^ Display.string_of_thm i_th1)
   15.47 +      val _ = Output.debug (fn () => "  isa th2 (neg): " ^ Display.string_of_thm i_th2)
   15.48      in
   15.49        if is_TrueI i_th1 then i_th2 (*Trivial cases where one operand is type info*)
   15.50        else if is_TrueI i_th2 then i_th1
   15.51 @@ -425,7 +425,7 @@
   15.52          val _ = Output.debug (fn () => "located term: " ^ Syntax.string_of_term ctxt tm_subst)
   15.53          val imax = maxidx_of_term (i_tm $ tm_abs $ tm_subst)  (*ill typed but gives right max*)
   15.54          val subst' = incr_indexes (imax+1) (if pos then subst_em else ssubst_em)
   15.55 -        val _ = Output.debug (fn () => "subst' " ^ string_of_thm subst')
   15.56 +        val _ = Output.debug (fn () => "subst' " ^ Display.string_of_thm subst')
   15.57          val eq_terms = map (pairself (cterm_of thy))
   15.58                             (ListPair.zip (term_vars (prop_of subst'), [tm_abs, tm_subst, i_tm]))
   15.59      in  cterm_instantiate eq_terms subst'  end;
   15.60 @@ -453,7 +453,7 @@
   15.61              val _ = Output.debug (fn () => "METIS THM: " ^ Metis.Thm.toString fol_th)
   15.62              val _ = Output.debug (fn () => "INFERENCE: " ^ Metis.Proof.inferenceToString inf)
   15.63              val th = Meson.flexflex_first_order (factor (step ctxt isFO thpairs (fol_th, inf)))
   15.64 -            val _ = Output.debug (fn () => "ISABELLE THM: " ^ string_of_thm th)
   15.65 +            val _ = Output.debug (fn () => "ISABELLE THM: " ^ Display.string_of_thm th)
   15.66              val _ = Output.debug (fn () => "=============================================")
   15.67              val n_metis_lits = length (filter real_literal (Metis.LiteralSet.toList (Metis.Thm.clause fol_th)))
   15.68          in
   15.69 @@ -572,9 +572,9 @@
   15.70          val _ = if exists(is_false o prop_of) cls then error "problem contains the empty clause"
   15.71                  else ();
   15.72          val _ = Output.debug (fn () => "FOL_SOLVE: CONJECTURE CLAUSES")
   15.73 -        val _ = app (fn th => Output.debug (fn () => string_of_thm th)) cls
   15.74 +        val _ = app (fn th => Output.debug (fn () => Display.string_of_thm th)) cls
   15.75          val _ = Output.debug (fn () => "THEOREM CLAUSES")
   15.76 -        val _ = app (fn th => Output.debug (fn () => string_of_thm th)) ths
   15.77 +        val _ = app (fn th => Output.debug (fn () => Display.string_of_thm th)) ths
   15.78          val {isFO,axioms,tfrees} = build_map mode ctxt cls ths
   15.79          val _ = if null tfrees then ()
   15.80                  else (Output.debug (fn () => "TFREE CLAUSES");
   15.81 @@ -597,13 +597,13 @@
   15.82                    val result = translate isFO ctxt' axioms proof
   15.83                    and used = List.mapPartial (used_axioms axioms) proof
   15.84                    val _ = Output.debug (fn () => "METIS COMPLETED...clauses actually used:")
   15.85 -	          val _ = app (fn th => Output.debug (fn () => string_of_thm th)) used
   15.86 +	          val _ = app (fn th => Output.debug (fn () => Display.string_of_thm th)) used
   15.87  	          val unused = filter (fn (a,cls) => not (common_thm used cls)) th_cls_pairs
   15.88                in
   15.89                    if null unused then ()
   15.90                    else warning ("Unused theorems: " ^ commas (map #1 unused));
   15.91                    case result of
   15.92 -                      (_,ith)::_ => (Output.debug (fn () => "success: " ^ string_of_thm ith); ith)
   15.93 +                      (_,ith)::_ => (Output.debug (fn () => "success: " ^ Display.string_of_thm ith); ith)
   15.94                      | _ => error "METIS: no result"
   15.95                end
   15.96            | Metis.Resolution.Satisfiable _ => error "Metis: No first-order proof with the lemmas supplied"
   15.97 @@ -611,7 +611,7 @@
   15.98  
   15.99    fun metis_general_tac mode ctxt ths i st0 =
  15.100      let val _ = Output.debug (fn () =>
  15.101 -          "Metis called with theorems " ^ cat_lines (map string_of_thm ths))
  15.102 +          "Metis called with theorems " ^ cat_lines (map Display.string_of_thm ths))
  15.103      in
  15.104         if exists_type ResAxioms.type_has_empty_sort (prop_of st0)  
  15.105         then error "Proof state contains the empty sort" else ();
    16.1 --- a/src/HOL/Tools/recfun_codegen.ML	Fri May 16 23:25:37 2008 +0200
    16.2 +++ b/src/HOL/Tools/recfun_codegen.ML	Sat May 17 13:54:30 2008 +0200
    16.3 @@ -32,7 +32,7 @@
    16.4  val const_of = dest_Const o head_of o fst o dest_eqn;
    16.5  
    16.6  fun warn thm = warning ("RecfunCodegen: Not a proper equation:\n" ^
    16.7 -  string_of_thm thm);
    16.8 +  Display.string_of_thm thm);
    16.9  
   16.10  fun add_thm opt_module thm =
   16.11    (if Pattern.pattern (lhs_of thm) then
    17.1 --- a/src/HOL/Tools/res_atp.ML	Fri May 16 23:25:37 2008 +0200
    17.2 +++ b/src/HOL/Tools/res_atp.ML	Sat May 17 13:54:30 2008 +0200
    17.3 @@ -498,10 +498,10 @@
    17.4          (foldl add_single_names (foldl add_multi_names [] mults) singles)
    17.5    end;
    17.6  
    17.7 -fun check_named ("",th) = (warning ("No name for theorem " ^ string_of_thm th); false)
    17.8 +fun check_named ("",th) = (warning ("No name for theorem " ^ Display.string_of_thm th); false)
    17.9    | check_named (_,th) = true;
   17.10  
   17.11 -fun display_thm (name,th) = Output.debug (fn () => name ^ ": " ^ string_of_thm th);
   17.12 +fun display_thm (name,th) = Output.debug (fn () => name ^ ": " ^ Display.string_of_thm th);
   17.13  
   17.14  (* get lemmas from claset, simpset, atpset and extra supplied rules *)
   17.15  fun get_clasimp_atp_lemmas ctxt user_thms =
   17.16 @@ -745,10 +745,10 @@
   17.17                  val _ = Output.debug (fn () => "About to write file " ^ fname)
   17.18                  val axcls = make_unique axcls
   17.19                  val _ = Output.debug (fn () => "Conjecture Clauses (before duplicate removal)")
   17.20 -                val _ = app (fn th => Output.debug (fn _ => string_of_thm th)) ccls
   17.21 +                val _ = app (fn th => Output.debug (fn _ => Display.string_of_thm th)) ccls
   17.22                  val ccls = subtract_cls ccls axcls
   17.23                  val _ = Output.debug (fn () => "Conjecture Clauses (AFTER duplicate removal)")
   17.24 -                val _ = app (fn th => Output.debug (fn _ => string_of_thm th)) ccls
   17.25 +                val _ = app (fn th => Output.debug (fn _ => Display.string_of_thm th)) ccls
   17.26                  val ccltms = map prop_of ccls
   17.27                  and axtms = map (prop_of o #1) axcls
   17.28                  val subs = tfree_classes_of_terms ccltms
   17.29 @@ -825,7 +825,7 @@
   17.30      Output.debug (fn () => "subgoals in isar_atp:\n" ^
   17.31                    Syntax.string_of_term ctxt (Logic.mk_conjunction_list (Thm.prems_of goal)));
   17.32      Output.debug (fn () => "current theory: " ^ Context.theory_name thy);
   17.33 -    app (fn th => Output.debug (fn _ => "chained: " ^ string_of_thm th)) chain_ths;
   17.34 +    app (fn th => Output.debug (fn _ => "chained: " ^ Display.string_of_thm th)) chain_ths;
   17.35      if !time_limit > 0 then isar_atp (ctxt, chain_ths, goal)
   17.36      else (warning ("Writing problem file only: " ^ !problem_name);
   17.37            isar_atp_writeonly (ctxt, chain_ths, goal))
    18.1 --- a/src/HOL/Tools/res_axioms.ML	Fri May 16 23:25:37 2008 +0200
    18.2 +++ b/src/HOL/Tools/res_axioms.ML	Sat May 17 13:54:30 2008 +0200
    18.3 @@ -176,7 +176,7 @@
    18.4  
    18.5  (*FIXME: requires more use of cterm constructors*)
    18.6  fun abstract ct =
    18.7 -  let val _ = Output.debug (fn()=>"  abstraction: " ^ string_of_cterm ct)
    18.8 +  let val _ = Output.debug (fn()=>"  abstraction: " ^ Display.string_of_cterm ct)
    18.9        val Abs(x,_,body) = term_of ct
   18.10        val thy = theory_of_cterm ct
   18.11        val Type("fun",[xT,bodyT]) = typ_of (ctyp_of_term ct)
   18.12 @@ -228,12 +228,12 @@
   18.13        Abs _ =>
   18.14  	let val (cv,cta) = Thm.dest_abs NONE ct
   18.15  	    val (v,Tv) = (dest_Free o term_of) cv
   18.16 -	    val _ = Output.debug (fn()=>"  recursion: " ^ string_of_cterm cta);
   18.17 +	    val _ = Output.debug (fn()=>"  recursion: " ^ Display.string_of_cterm cta);
   18.18  	    val u_th = combinators_aux cta
   18.19 -	    val _ = Output.debug (fn()=>"  returned " ^ string_of_thm u_th);
   18.20 +	    val _ = Output.debug (fn()=>"  returned " ^ Display.string_of_thm u_th);
   18.21  	    val cu = Thm.rhs_of u_th
   18.22  	    val comb_eq = abstract (Thm.cabs cv cu)
   18.23 -	in Output.debug (fn()=>"  abstraction result: " ^ string_of_thm comb_eq);
   18.24 +	in Output.debug (fn()=>"  abstraction result: " ^ Display.string_of_thm comb_eq);
   18.25  	   (transitive (abstract_rule v cv u_th) comb_eq) end
   18.26      | t1 $ t2 =>
   18.27  	let val (ct1,ct2) = Thm.dest_comb ct
   18.28 @@ -242,13 +242,13 @@
   18.29  fun combinators th =
   18.30    if lambda_free (prop_of th) then th 
   18.31    else
   18.32 -    let val _ = Output.debug (fn()=>"Conversion to combinators: " ^ string_of_thm th);
   18.33 +    let val _ = Output.debug (fn()=>"Conversion to combinators: " ^ Display.string_of_thm th);
   18.34  	val th = Drule.eta_contraction_rule th
   18.35  	val eqth = combinators_aux (cprop_of th)
   18.36 -	val _ = Output.debug (fn()=>"Conversion result: " ^ string_of_thm eqth);
   18.37 +	val _ = Output.debug (fn()=>"Conversion result: " ^ Display.string_of_thm eqth);
   18.38      in  equal_elim eqth th   end
   18.39      handle THM (msg,_,_) => 
   18.40 -      (warning ("Error in the combinator translation of " ^ string_of_thm th);
   18.41 +      (warning ("Error in the combinator translation of " ^ Display.string_of_thm th);
   18.42         warning ("  Exception message: " ^ msg);
   18.43         TrueI);  (*A type variable of sort {} will cause make abstraction fail.*)
   18.44  
   18.45 @@ -311,7 +311,7 @@
   18.46  fun assert_lambda_free ths msg =
   18.47    case filter (not o lambda_free o prop_of) ths of
   18.48        [] => ()
   18.49 -    | ths' => error (msg ^ "\n" ^ cat_lines (map string_of_thm ths'));
   18.50 +    | ths' => error (msg ^ "\n" ^ cat_lines (map Display.string_of_thm ths'));
   18.51  
   18.52  
   18.53  (*** Blacklisting (duplicated in ResAtp? ***)
   18.54 @@ -367,7 +367,7 @@
   18.55  
   18.56  fun name_or_string th =
   18.57    if PureThy.has_name_hint th then PureThy.get_name_hint th
   18.58 -  else string_of_thm th;
   18.59 +  else Display.string_of_thm th;
   18.60  
   18.61  (*Declare Skolem functions for a theorem, supplied in nnf and with its name.
   18.62    It returns a modified theory, unless skolemization fails.*)
   18.63 @@ -378,7 +378,7 @@
   18.64       Option.map
   18.65          (fn (nnfth,ctxt1) =>
   18.66            let 
   18.67 -              val _ = Output.debug (fn () => "  initial nnf: " ^ string_of_thm nnfth)
   18.68 +              val _ = Output.debug (fn () => "  initial nnf: " ^ Display.string_of_thm nnfth)
   18.69                val s = fake_name th
   18.70                val (thy',defs) = declare_skofuns s nnfth thy
   18.71                val (cnfs,ctxt2) = Meson.make_cnf (map skolem_of_def defs) nnfth ctxt1
   18.72 @@ -531,15 +531,15 @@
   18.73                                        (map Thm.term_of hyps)
   18.74        val fixed = term_frees (concl_of st) @
   18.75                    foldl (gen_union (op aconv)) [] (map term_frees remaining_hyps)
   18.76 -  in  Output.debug (fn _ => "expand_defs_tac: " ^ string_of_thm st);
   18.77 -      Output.debug (fn _ => "  st0: " ^ string_of_thm st0);
   18.78 -      Output.debug (fn _ => "  defs: " ^ commas (map string_of_cterm defs));
   18.79 +  in  Output.debug (fn _ => "expand_defs_tac: " ^ Display.string_of_thm st);
   18.80 +      Output.debug (fn _ => "  st0: " ^ Display.string_of_thm st0);
   18.81 +      Output.debug (fn _ => "  defs: " ^ commas (map Display.string_of_cterm defs));
   18.82        Seq.of_list [LocalDefs.expand (filter (is_okdef fixed o Thm.term_of) defs) st]
   18.83    end;
   18.84  
   18.85  
   18.86  fun meson_general_tac ths i st0 =
   18.87 - let val _ = Output.debug (fn () => "Meson called: " ^ cat_lines (map string_of_thm ths))
   18.88 + let val _ = Output.debug (fn () => "Meson called: " ^ cat_lines (map Display.string_of_thm ths))
   18.89   in  (Meson.meson_claset_tac (cnf_rules_of_ths ths) HOL_cs i THEN expand_defs_tac st0) st0 end;
   18.90  
   18.91  val meson_method_setup = Method.add_methods
    19.1 --- a/src/HOL/Tools/res_reconstruct.ML	Fri May 16 23:25:37 2008 +0200
    19.2 +++ b/src/HOL/Tools/res_reconstruct.ML	Sat May 17 13:54:30 2008 +0200
    19.3 @@ -38,7 +38,7 @@
    19.4  fun trace s = if !Output.debugging then File.append (File.tmp_path trace_path) s
    19.5                else ();
    19.6  
    19.7 -val string_of_thm = PrintMode.setmp [] string_of_thm;
    19.8 +val string_of_thm = PrintMode.setmp [] Display.string_of_thm;
    19.9  
   19.10  (*For generating structured proofs: keep every nth proof line*)
   19.11  val (modulus, modulus_setup) = Attrib.config_int "sledgehammer_modulus" 1;
    20.1 --- a/src/HOL/Tools/sat_funcs.ML	Fri May 16 23:25:37 2008 +0200
    20.2 +++ b/src/HOL/Tools/sat_funcs.ML	Sat May 17 13:54:30 2008 +0200
    20.3 @@ -164,8 +164,8 @@
    20.4  		fun resolution (c1, hyps1) (c2, hyps2) =
    20.5  		let
    20.6  			val _ = if !trace_sat then
    20.7 -					tracing ("Resolving clause: " ^ string_of_thm c1 ^ " (hyps: " ^ ML_Syntax.print_list (Sign.string_of_term (theory_of_thm c1)) (#hyps (rep_thm c1))
    20.8 -						^ ")\nwith clause: " ^ string_of_thm c2 ^ " (hyps: " ^ ML_Syntax.print_list (Sign.string_of_term (theory_of_thm c2)) (#hyps (rep_thm c2)) ^ ")")
    20.9 +					tracing ("Resolving clause: " ^ Display.string_of_thm c1 ^ " (hyps: " ^ ML_Syntax.print_list (Sign.string_of_term (theory_of_thm c1)) (#hyps (rep_thm c1))
   20.10 +						^ ")\nwith clause: " ^ Display.string_of_thm c2 ^ " (hyps: " ^ ML_Syntax.print_list (Sign.string_of_term (theory_of_thm c2)) (#hyps (rep_thm c2)) ^ ")")
   20.11  				else ()
   20.12  
   20.13  			(* the two literals used for resolution *)
   20.14 @@ -182,7 +182,7 @@
   20.15  				end
   20.16  
   20.17  			val _ = if !trace_sat then
   20.18 -					tracing ("Resolution theorem: " ^ string_of_thm res_thm)
   20.19 +					tracing ("Resolution theorem: " ^ Display.string_of_thm res_thm)
   20.20  				else ()
   20.21  
   20.22  			(* Gamma1, Gamma2 |- False *)
   20.23 @@ -191,7 +191,7 @@
   20.24  				(if hyp1_is_neg then c1' else c2')
   20.25  
   20.26  			val _ = if !trace_sat then
   20.27 -					tracing ("Resulting clause: " ^ string_of_thm c_new ^ " (hyps: " ^ ML_Syntax.print_list (Sign.string_of_term (theory_of_thm c_new)) (#hyps (rep_thm c_new)) ^ ")")
   20.28 +					tracing ("Resulting clause: " ^ Display.string_of_thm c_new ^ " (hyps: " ^ ML_Syntax.print_list (Sign.string_of_term (theory_of_thm c_new)) (#hyps (rep_thm c_new)) ^ ")")
   20.29  				else ()
   20.30  			val _ = inc counter
   20.31  		in
   20.32 @@ -312,7 +312,7 @@
   20.33  		((cnf.is_clause o HOLogic.dest_Trueprop o Thm.term_of) clause
   20.34  			handle TERM ("dest_Trueprop", _) => false)
   20.35  		orelse (
   20.36 -			warning ("Ignoring non-clausal premise " ^ string_of_cterm clause);
   20.37 +			warning ("Ignoring non-clausal premise " ^ Display.string_of_cterm clause);
   20.38  			false)) clauses'
   20.39  	(* remove trivial clauses -- this is necessary because zChaff removes *)
   20.40  	(* trivial clauses during preprocessing, and otherwise our clause     *)
   20.41 @@ -325,7 +325,7 @@
   20.42  	(* sorted in ascending order                                          *)
   20.43  	val sorted_clauses = sort (Term.fast_term_ord o pairself Thm.term_of) nontrivial_clauses
   20.44  	val _ = if !trace_sat then
   20.45 -			tracing ("Sorted non-trivial clauses:\n" ^ space_implode "\n" (map string_of_cterm sorted_clauses))
   20.46 +			tracing ("Sorted non-trivial clauses:\n" ^ space_implode "\n" (map Display.string_of_cterm sorted_clauses))
   20.47  		else ()
   20.48  	(* translate clauses from HOL terms to PropLogic.prop_formula *)
   20.49  	val (fms, atom_table) = fold_map (PropLogic.prop_formula_of_term o HOLogic.dest_Trueprop o Thm.term_of) sorted_clauses Termtab.empty
    21.1 --- a/src/HOL/Tools/specification_package.ML	Fri May 16 23:25:37 2008 +0200
    21.2 +++ b/src/HOL/Tools/specification_package.ML	Sat May 17 13:54:30 2008 +0200
    21.3 @@ -184,7 +184,7 @@
    21.4                          fun add_final (arg as (thy, thm)) =
    21.5                              if name = ""
    21.6                              then arg |> Library.swap
    21.7 -                            else (writeln ("  " ^ name ^ ": " ^ (string_of_thm thm));
    21.8 +                            else (writeln ("  " ^ name ^ ": " ^ (Display.string_of_thm thm));
    21.9                                    PureThy.store_thm (name, thm) thy)
   21.10                      in
   21.11                          args |> apsnd (remove_alls frees)
    22.1 --- a/src/HOL/Tools/watcher.ML	Fri May 16 23:25:37 2008 +0200
    22.2 +++ b/src/HOL/Tools/watcher.ML	Sat May 17 13:54:30 2008 +0200
    22.3 @@ -343,10 +343,10 @@
    22.4    handle OS.SysErr _ => ()
    22.5  
    22.6  fun string_of_subgoal th i =
    22.7 -    string_of_cterm (List.nth(cprems_of th, i-1))
    22.8 +    Display.string_of_cterm (List.nth(cprems_of th, i-1))
    22.9      handle Subscript => "Subgoal number out of range!"
   22.10  
   22.11 -fun prems_string_of th = space_implode "\n" (map string_of_cterm (cprems_of th))
   22.12 +fun prems_string_of th = space_implode "\n" (map Display.string_of_cterm (cprems_of th))
   22.13  
   22.14  fun read_proof probfile =
   22.15    let val p = ResReconstruct.txt_path probfile
    23.1 --- a/src/Provers/blast.ML	Fri May 16 23:25:37 2008 +0200
    23.2 +++ b/src/Provers/blast.ML	Sat May 17 13:54:30 2008 +0200
    23.3 @@ -495,7 +495,7 @@
    23.4  end;
    23.5  
    23.6  
    23.7 -fun TRACE rl tac st i = if !trace then (prth rl; tac st i) else tac st i;
    23.8 +fun TRACE rl tac st i = if !trace then (Display.prth rl; tac st i) else tac st i;
    23.9  
   23.10  (*Resolution/matching tactics: if upd then the proof state may be updated.
   23.11    Matching makes the tactics more deterministic in the presence of Vars.*)
   23.12 @@ -513,11 +513,11 @@
   23.13          rot_subgoals_tac (rot, #2 trl) i
   23.14    in Option.SOME (trl, tac) end
   23.15    handle ElimBadPrem => (*reject: prems don't preserve conclusion*)
   23.16 -            (warning("Ignoring weak elimination rule\n" ^ string_of_thm rl);
   23.17 +            (warning("Ignoring weak elimination rule\n" ^ Display.string_of_thm rl);
   23.18               Option.NONE)
   23.19         | ElimBadConcl => (*ignore: conclusion is not just a variable*)
   23.20             (if !trace then (warning("Ignoring ill-formed elimination rule:\n" ^
   23.21 -                       "conclusion should be a variable\n" ^ string_of_thm rl))
   23.22 +                       "conclusion should be a variable\n" ^ Display.string_of_thm rl))
   23.23              else ();
   23.24              Option.NONE);
   23.25  
    24.1 --- a/src/Provers/classical.ML	Fri May 16 23:25:37 2008 +0200
    24.2 +++ b/src/Provers/classical.ML	Sat May 17 13:54:30 2008 +0200
    24.3 @@ -338,13 +338,13 @@
    24.4    is still allowed.*)
    24.5  fun warn_dup th (CS{safeIs, safeEs, hazIs, hazEs, ...}) =
    24.6         if mem_thm safeIs th then
    24.7 -         warning ("Rule already declared as safe introduction (intro!)\n" ^ string_of_thm th)
    24.8 +         warning ("Rule already declared as safe introduction (intro!)\n" ^ Display.string_of_thm th)
    24.9    else if mem_thm safeEs th then
   24.10 -         warning ("Rule already declared as safe elimination (elim!)\n" ^ string_of_thm th)
   24.11 +         warning ("Rule already declared as safe elimination (elim!)\n" ^ Display.string_of_thm th)
   24.12    else if mem_thm hazIs th then
   24.13 -         warning ("Rule already declared as introduction (intro)\n" ^ string_of_thm th)
   24.14 +         warning ("Rule already declared as introduction (intro)\n" ^ Display.string_of_thm th)
   24.15    else if mem_thm hazEs th then
   24.16 -         warning ("Rule already declared as elimination (elim)\n" ^ string_of_thm th)
   24.17 +         warning ("Rule already declared as elimination (elim)\n" ^ Display.string_of_thm th)
   24.18    else ();
   24.19  
   24.20  
   24.21 @@ -354,7 +354,7 @@
   24.22    (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   24.23               safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   24.24    if mem_thm safeIs th then
   24.25 -         (warning ("Ignoring duplicate safe introduction (intro!)\n" ^ string_of_thm th);
   24.26 +         (warning ("Ignoring duplicate safe introduction (intro!)\n" ^ Display.string_of_thm th);
   24.27            cs)
   24.28    else
   24.29    let val th' = flat_rule th
   24.30 @@ -380,10 +380,10 @@
   24.31    (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   24.32               safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   24.33    if mem_thm safeEs th then
   24.34 -         (warning ("Ignoring duplicate safe elimination (elim!)\n" ^ string_of_thm th);
   24.35 +         (warning ("Ignoring duplicate safe elimination (elim!)\n" ^ Display.string_of_thm th);
   24.36            cs)
   24.37    else if has_fewer_prems 1 th then
   24.38 -    	error("Ill-formed elimination rule\n" ^ string_of_thm th)
   24.39 +    	error("Ill-formed elimination rule\n" ^ Display.string_of_thm th)
   24.40    else
   24.41    let
   24.42        val th' = classical_rule (flat_rule th)
   24.43 @@ -410,7 +410,7 @@
   24.44  
   24.45  fun make_elim th =
   24.46      if has_fewer_prems 1 th then
   24.47 -    	error("Ill-formed destruction rule\n" ^ string_of_thm th)
   24.48 +    	error("Ill-formed destruction rule\n" ^ Display.string_of_thm th)
   24.49      else Tactic.make_elim th;
   24.50  
   24.51  fun cs addSDs ths = cs addSEs (map make_elim ths);
   24.52 @@ -422,7 +422,7 @@
   24.53    (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   24.54               safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   24.55    if mem_thm hazIs th then
   24.56 -         (warning ("Ignoring duplicate introduction (intro)\n" ^ string_of_thm th);
   24.57 +         (warning ("Ignoring duplicate introduction (intro)\n" ^ Display.string_of_thm th);
   24.58            cs)
   24.59    else
   24.60    let val th' = flat_rule th
   24.61 @@ -442,16 +442,16 @@
   24.62          xtra_netpair = insert' (the_default 1 w) (nI,nE) ([th], []) xtra_netpair}
   24.63    end
   24.64    handle THM("RSN: no unifiers",_,_) => (*from dup_intr*)
   24.65 -         error ("Ill-formed introduction rule\n" ^ string_of_thm th);
   24.66 +         error ("Ill-formed introduction rule\n" ^ Display.string_of_thm th);
   24.67  
   24.68  fun addE w th
   24.69    (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   24.70              safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   24.71    if mem_thm hazEs th then
   24.72 -         (warning ("Ignoring duplicate elimination (elim)\n" ^ string_of_thm th);
   24.73 +         (warning ("Ignoring duplicate elimination (elim)\n" ^ Display.string_of_thm th);
   24.74            cs)
   24.75    else if has_fewer_prems 1 th then
   24.76 -    	error("Ill-formed elimination rule\n" ^ string_of_thm th)
   24.77 +    	error("Ill-formed elimination rule\n" ^ Display.string_of_thm th)
   24.78    else
   24.79    let
   24.80        val th' = classical_rule (flat_rule th)
   24.81 @@ -543,7 +543,7 @@
   24.82      end
   24.83   else cs
   24.84   handle THM("RSN: no unifiers",_,_) => (*from dup_intr*)
   24.85 -        error ("Ill-formed introduction rule\n" ^ string_of_thm th);
   24.86 +        error ("Ill-formed introduction rule\n" ^ Display.string_of_thm th);
   24.87  
   24.88  
   24.89  fun delE th
   24.90 @@ -572,7 +572,7 @@
   24.91        mem_thm hazIs th orelse mem_thm hazEs th orelse
   24.92        mem_thm safeEs th' orelse mem_thm hazEs th'
   24.93      then delSI th (delSE th (delI th (delE th (delSE th' (delE th' cs)))))
   24.94 -    else (warning ("Undeclared classical rule\n" ^ string_of_thm th); cs)
   24.95 +    else (warning ("Undeclared classical rule\n" ^ Display.string_of_thm th); cs)
   24.96    end;
   24.97  
   24.98  fun cs delrules ths = fold delrule ths cs;
    25.1 --- a/src/Pure/Isar/code.ML	Fri May 16 23:25:37 2008 +0200
    25.2 +++ b/src/Pure/Isar/code.ML	Sat May 17 13:54:30 2008 +0200
    25.3 @@ -116,7 +116,7 @@
    25.4  (** certificate theorems **)
    25.5  
    25.6  fun string_of_lthms r = case Susp.peek r
    25.7 - of SOME thms => (map string_of_thm o rev) thms
    25.8 + of SOME thms => (map Display.string_of_thm o rev) thms
    25.9    | NONE => ["[...]"];
   25.10  
   25.11  fun pretty_lthms ctxt r = case Susp.peek r
   25.12 @@ -147,7 +147,7 @@
   25.13        | matches (_ :: _) [] = false
   25.14        | matches (x :: xs) (y :: ys) = Pattern.matches thy (x, y) andalso matches xs ys;
   25.15      fun drop thm' = not (matches args (args_of thm'))
   25.16 -      orelse (warning ("code generator: dropping redundant defining equation\n" ^ string_of_thm thm'); false);
   25.17 +      orelse (warning ("code generator: dropping redundant defining equation\n" ^ Display.string_of_thm thm'); false);
   25.18      val (keeps, drops) = List.partition drop sels;
   25.19    in (thm :: keeps, dels |> remove Thm.eq_thm_prop thm |> fold (insert Thm.eq_thm_prop) drops) end;
   25.20  
   25.21 @@ -537,7 +537,7 @@
   25.22    let
   25.23      fun cert thm = if const = const_of_func thy thm
   25.24        then thm else error ("Wrong head of defining equation,\nexpected constant "
   25.25 -        ^ CodeUnit.string_of_const thy const ^ "\n" ^ string_of_thm thm)
   25.26 +        ^ CodeUnit.string_of_const thy const ^ "\n" ^ Display.string_of_thm thm)
   25.27    in map cert thms end;
   25.28  
   25.29  
   25.30 @@ -655,13 +655,13 @@
   25.31              then thm
   25.32              else (warning ("Constraining type\n" ^ CodeUnit.string_of_typ thy ty
   25.33                ^ "\nof defining equation\n"
   25.34 -              ^ string_of_thm thm
   25.35 +              ^ Display.string_of_thm thm
   25.36                ^ "\nto permitted most general type\n"
   25.37                ^ CodeUnit.string_of_typ thy ty_decl);
   25.38                constrain thm)
   25.39              else CodeUnit.bad_thm ("Type\n" ^ CodeUnit.string_of_typ thy ty
   25.40                ^ "\nof defining equation\n"
   25.41 -              ^ string_of_thm thm
   25.42 +              ^ Display.string_of_thm thm
   25.43                ^ "\nis incompatible with permitted least general type\n"
   25.44                ^ CodeUnit.string_of_typ thy ty_strongest)
   25.45            end;
   25.46 @@ -673,7 +673,7 @@
   25.47          then thm
   25.48          else CodeUnit.bad_thm ("Type\n" ^ CodeUnit.string_of_typ thy ty
   25.49             ^ "\nof defining equation\n"
   25.50 -           ^ string_of_thm thm
   25.51 +           ^ Display.string_of_thm thm
   25.52             ^ "\nis incompatible with declared function type\n"
   25.53             ^ CodeUnit.string_of_typ thy ty_decl)
   25.54        end;
   25.55 @@ -731,11 +731,11 @@
   25.56      val c = const_of_func thy func;
   25.57      val _ = if (is_some o AxClass.class_of_param thy) c
   25.58        then error ("Rejected polymorphic equation for overloaded constant:\n"
   25.59 -        ^ string_of_thm thm)
   25.60 +        ^ Display.string_of_thm thm)
   25.61        else ();
   25.62      val _ = if (is_some o get_datatype_of_constr thy) c
   25.63        then error ("Rejected equation for datatype constructor:\n"
   25.64 -        ^ string_of_thm func)
   25.65 +        ^ Display.string_of_thm func)
   25.66        else ();
   25.67    in
   25.68      (map_exec_purge (SOME [c]) o map_funcs) (Symtab.map_default
    26.1 --- a/src/Pure/display.ML	Fri May 16 23:25:37 2008 +0200
    26.2 +++ b/src/Pure/display.ML	Sat May 17 13:54:30 2008 +0200
    26.3 @@ -11,17 +11,6 @@
    26.4    val goals_limit: int ref
    26.5    val show_hyps: bool ref
    26.6    val show_tags: bool ref
    26.7 -  val string_of_thm: thm -> string
    26.8 -  val print_thm: thm -> unit
    26.9 -  val print_thms: thm list -> unit
   26.10 -  val prth: thm -> thm
   26.11 -  val prthq: thm Seq.seq -> thm Seq.seq
   26.12 -  val prths: thm list -> thm list
   26.13 -  val string_of_ctyp: ctyp -> string
   26.14 -  val print_ctyp: ctyp -> unit
   26.15 -  val string_of_cterm: cterm -> string
   26.16 -  val print_cterm: cterm -> unit
   26.17 -  val print_syntax: theory -> unit
   26.18    val show_consts: bool ref
   26.19  end;
   26.20  
   26.21 @@ -31,11 +20,22 @@
   26.22    val pretty_flexpair: Pretty.pp -> term * term -> Pretty.T
   26.23    val pretty_thm_aux: Pretty.pp -> bool -> bool -> term list -> thm -> Pretty.T
   26.24    val pretty_thm: thm -> Pretty.T
   26.25 +  val string_of_thm: thm -> string
   26.26    val pretty_thms: thm list -> Pretty.T
   26.27    val pretty_thm_sg: theory -> thm -> Pretty.T
   26.28    val pretty_thms_sg: theory -> thm list -> Pretty.T
   26.29 +  val print_thm: thm -> unit
   26.30 +  val print_thms: thm list -> unit
   26.31 +  val prth: thm -> thm
   26.32 +  val prthq: thm Seq.seq -> thm Seq.seq
   26.33 +  val prths: thm list -> thm list
   26.34    val pretty_ctyp: ctyp -> Pretty.T
   26.35 +  val string_of_ctyp: ctyp -> string
   26.36 +  val print_ctyp: ctyp -> unit
   26.37    val pretty_cterm: cterm -> Pretty.T
   26.38 +  val string_of_cterm: cterm -> string
   26.39 +  val print_cterm: cterm -> unit
   26.40 +  val print_syntax: theory -> unit
   26.41    val pretty_full_theory: bool -> theory -> Pretty.T list
   26.42    val pretty_goals_aux: Pretty.pp -> Markup.T -> bool * bool -> int -> thm -> Pretty.T list
   26.43    val pretty_goals: int -> thm -> Pretty.T list
    27.1 --- a/src/Pure/old_goals.ML	Fri May 16 23:25:37 2008 +0200
    27.2 +++ b/src/Pure/old_goals.ML	Sat May 17 13:54:30 2008 +0200
    27.3 @@ -201,7 +201,7 @@
    27.4    case e of
    27.5       THM (msg,i,thms) =>
    27.6           (writeln ("Exception THM " ^ string_of_int i ^ " raised:\n" ^ msg);
    27.7 -          List.app print_thm thms)
    27.8 +          List.app Display.print_thm thms)
    27.9     | THEORY (msg,thys) =>
   27.10           (writeln ("Exception THEORY raised:\n" ^ msg);
   27.11            List.app (writeln o Context.str_of_thy) thys)
    28.1 --- a/src/Sequents/prover.ML	Fri May 16 23:25:37 2008 +0200
    28.2 +++ b/src/Sequents/prover.ML	Sat May 17 13:54:30 2008 +0200
    28.3 @@ -28,7 +28,7 @@
    28.4  
    28.5  fun warn_duplicates [] = []
    28.6    | warn_duplicates dups =
    28.7 -      (warning (cat_lines ("Ignoring duplicate theorems:" :: map string_of_thm dups));
    28.8 +      (warning (cat_lines ("Ignoring duplicate theorems:" :: map Display.string_of_thm dups));
    28.9         dups);
   28.10  
   28.11  fun (Pack(safes,unsafes)) add_safes ths   = 
   28.12 @@ -51,8 +51,8 @@
   28.13  
   28.14  
   28.15  fun print_pack (Pack(safes,unsafes)) =
   28.16 -    (writeln "Safe rules:";  print_thms safes;
   28.17 -     writeln "Unsafe rules:"; print_thms unsafes);
   28.18 +    (writeln "Safe rules:";  Display.print_thms safes;
   28.19 +     writeln "Unsafe rules:"; Display.print_thms unsafes);
   28.20  
   28.21  (*Returns the list of all formulas in the sequent*)
   28.22  fun forms_of_seq (Const("SeqO'",_) $ P $ u) = P :: forms_of_seq u
    29.1 --- a/src/Sequents/simpdata.ML	Fri May 16 23:25:37 2008 +0200
    29.2 +++ b/src/Sequents/simpdata.ML	Sat May 17 13:54:30 2008 +0200
    29.3 @@ -126,7 +126,7 @@
    29.4                      | (Const("Not",_)$_)      => th RS iff_reflection_F
    29.5                      | _                       => th RS iff_reflection_T)
    29.6             | _ => error ("addsimps: unable to use theorem\n" ^
    29.7 -                         string_of_thm th));
    29.8 +                         Display.string_of_thm th));
    29.9  
   29.10  (*Replace premises x=y, X<->Y by X==Y*)
   29.11  val mk_meta_prems =
    30.1 --- a/src/Tools/code/code_funcgr.ML	Fri May 16 23:25:37 2008 +0200
    30.2 +++ b/src/Tools/code/code_funcgr.ML	Sat May 17 13:54:30 2008 +0200
    30.3 @@ -118,7 +118,7 @@
    30.4              handle Sorts.CLASS_ERROR e => raise CLASS_ERROR ([c], Sorts.class_error pp e ^ ",\n"
    30.5                ^ "for constant " ^ CodeUnit.string_of_const thy c
    30.6                ^ "\nin defining equations(s)\n"
    30.7 -              ^ (cat_lines o map string_of_thm) thms)
    30.8 +              ^ (cat_lines o map Display.string_of_thm) thms)
    30.9              (*handle Sorts.CLASS_ERROR _ => tab (*permissive!*)*)
   30.10            end;
   30.11          fun match (c, ty) = case tap_typ c
   30.12 @@ -225,7 +225,7 @@
   30.13                  else raise CLASS_ERROR ([c], "Illegal instantation for class operation "
   30.14                    ^ CodeUnit.string_of_const thy c
   30.15                    ^ "\nin defining equations\n"
   30.16 -                  ^ (cat_lines o map (string_of_thm o AxClass.overload thy)) thms)
   30.17 +                  ^ (cat_lines o map (Display.string_of_thm o AxClass.overload thy)) thms)
   30.18                end
   30.19            | NONE => (snd o CodeUnit.head_func) thm;
   30.20      fun add_funcs (const, thms) =
   30.21 @@ -304,7 +304,7 @@
   30.22        in
   30.23          Thm.transitive thm1 (Thm.transitive thm2 thm3) handle THM _ =>
   30.24            error ("could not construct evaluation proof (probably due to wellsortedness problem):\n"
   30.25 -          ^ (cat_lines o map string_of_thm) [thm1, thm2, thm3])
   30.26 +          ^ (cat_lines o map Display.string_of_thm) [thm1, thm2, thm3])
   30.27        end;
   30.28    in proto_eval thy I evaluator end;
   30.29  
    31.1 --- a/src/ZF/Datatype_ZF.thy	Fri May 16 23:25:37 2008 +0200
    31.2 +++ b/src/ZF/Datatype_ZF.thy	Sat May 17 13:54:30 2008 +0200
    31.3 @@ -72,7 +72,7 @@
    31.4  
    31.5   fun proc sg ss old =
    31.6     let val _ = if !trace then writeln ("data_free: OLD = " ^ 
    31.7 -                                       string_of_cterm (cterm_of sg old))
    31.8 +                                       Display.string_of_cterm (cterm_of sg old))
    31.9                 else ()
   31.10         val (lhs,rhs) = FOLogic.dest_eq old
   31.11         val (lhead, largs) = strip_comb lhs
   31.12 @@ -90,7 +90,7 @@
   31.13                 else Const("False",FOLogic.oT)
   31.14             else raise Match
   31.15         val _ = if !trace then 
   31.16 -                 writeln ("NEW = " ^ string_of_cterm (Thm.cterm_of sg new))
   31.17 +                 writeln ("NEW = " ^ Display.string_of_cterm (Thm.cterm_of sg new))
   31.18                 else ();
   31.19         val goal = Logic.mk_equals (old, new)
   31.20         val thm = Goal.prove (Simplifier.the_context ss) [] [] goal
    32.1 --- a/src/ZF/Tools/inductive_package.ML	Fri May 16 23:25:37 2008 +0200
    32.2 +++ b/src/ZF/Tools/inductive_package.ML	Sat May 17 13:54:30 2008 +0200
    32.3 @@ -250,7 +250,7 @@
    32.4      |> ListPair.map (fn (t, tacs) =>
    32.5        Goal.prove_global thy1 [] [] t
    32.6          (fn _ => EVERY (rewrite_goals_tac part_rec_defs :: tacs)))
    32.7 -    handle MetaSimplifier.SIMPLIFIER (msg, thm) => (print_thm thm; error msg);
    32.8 +    handle MetaSimplifier.SIMPLIFIER (msg, thm) => (Display.print_thm thm; error msg);
    32.9  
   32.10    (********)
   32.11    val dummy = writeln "  Proving the elimination rule...";
   32.12 @@ -325,7 +325,7 @@
   32.13       val dummy = if !Ind_Syntax.trace then
   32.14                   (writeln "ind_prems = ";
   32.15                    List.app (writeln o Syntax.string_of_term ctxt1) ind_prems;
   32.16 -                  writeln "raw_induct = "; print_thm raw_induct)
   32.17 +                  writeln "raw_induct = "; Display.print_thm raw_induct)
   32.18               else ();
   32.19  
   32.20  
   32.21 @@ -356,7 +356,7 @@
   32.22              ind_tac (rev (map (rewrite_rule part_rec_defs) prems)) (length prems)]);
   32.23  
   32.24       val dummy = if !Ind_Syntax.trace then
   32.25 -                 (writeln "quant_induct = "; print_thm quant_induct)
   32.26 +                 (writeln "quant_induct = "; Display.print_thm quant_induct)
   32.27               else ();
   32.28  
   32.29  
   32.30 @@ -431,7 +431,7 @@
   32.31         else (writeln "  [ No mutual induction rule needed ]"; @{thm TrueI});
   32.32  
   32.33       val dummy = if !Ind_Syntax.trace then
   32.34 -                 (writeln "lemma = "; print_thm lemma)
   32.35 +                 (writeln "lemma = "; Display.print_thm lemma)
   32.36               else ();
   32.37  
   32.38