proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
authorwenzelm
Tue Jul 21 01:03:18 2009 +0200 (2009-07-21)
changeset 3209130e2ffbba718
parent 32090 39acf19e9f3a
child 32092 6a5995438266
proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
src/FOLP/classical.ML
src/FOLP/ex/Prolog.ML
src/FOLP/simp.ML
src/HOL/Import/import.ML
src/HOL/Import/proof_kernel.ML
src/HOL/Import/shuffler.ML
src/HOL/Nominal/nominal_thmdecls.ML
src/HOL/Tools/TFL/casesplit.ML
src/HOL/Tools/TFL/rules.ML
src/HOL/Tools/TFL/tfl.ML
src/HOL/Tools/atp_minimal.ML
src/HOL/Tools/atp_wrapper.ML
src/HOL/Tools/choice_specification.ML
src/HOL/Tools/inductive.ML
src/HOL/Tools/inductive_codegen.ML
src/HOL/Tools/inductive_realizer.ML
src/HOL/Tools/lin_arith.ML
src/HOL/Tools/meson.ML
src/HOL/Tools/metis_tools.ML
src/HOL/Tools/recdef.ML
src/HOL/Tools/record.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/ex/predicate_compile.ML
src/Provers/Arith/fast_lin_arith.ML
src/Provers/blast.ML
src/Provers/classical.ML
src/Pure/Isar/args.ML
src/Pure/Isar/calculation.ML
src/Pure/Isar/code.ML
src/Pure/Isar/context_rules.ML
src/Pure/Isar/element.ML
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/local_defs.ML
src/Pure/Isar/method.ML
src/Pure/Isar/obtain.ML
src/Pure/Isar/proof.ML
src/Pure/Isar/proof_display.ML
src/Pure/Isar/runtime.ML
src/Pure/ProofGeneral/proof_general_pgip.ML
src/Pure/Tools/find_theorems.ML
src/Pure/old_goals.ML
src/Pure/simplifier.ML
src/Sequents/prover.ML
src/Sequents/simpdata.ML
src/Tools/Code/code_preproc.ML
src/Tools/Code/code_printer.ML
src/Tools/Code/code_thingol.ML
src/Tools/coherent.ML
src/Tools/induct.ML
src/ZF/Tools/inductive_package.ML
src/ZF/Tools/typechk.ML
     1.1 --- a/src/FOLP/classical.ML	Tue Jul 21 00:56:19 2009 +0200
     1.2 +++ b/src/FOLP/classical.ML	Tue Jul 21 01:03:18 2009 +0200
     1.3 @@ -124,11 +124,11 @@
     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";  Display.prths hazIs;
     1.8 -  writeln"Safe introduction rules";  Display.prths safeIs;
     1.9 -  writeln"Elimination rules";  Display.prths hazEs;
    1.10 -  writeln"Safe elimination rules";  Display.prths safeEs;
    1.11 -  ());
    1.12 +  writeln (cat_lines
    1.13 +   (["Introduction rules"] @ map Display.string_of_thm_without_context hazIs @
    1.14 +    ["Safe introduction rules"] @ map Display.string_of_thm_without_context safeIs @
    1.15 +    ["Elimination rules"] @ map Display.string_of_thm_without_context hazEs @
    1.16 +    ["Safe elimination rules"] @ map Display.string_of_thm_without_context safeEs));
    1.17  
    1.18  fun (CS{safeIs,safeEs,hazIs,hazEs,...}) addSIs ths =
    1.19    make_cs {safeIs=ths@safeIs, safeEs=safeEs, hazIs=hazIs, hazEs=hazEs};
     2.1 --- a/src/FOLP/ex/Prolog.ML	Tue Jul 21 00:56:19 2009 +0200
     2.2 +++ b/src/FOLP/ex/Prolog.ML	Tue Jul 21 01:03:18 2009 +0200
     2.3 @@ -13,7 +13,7 @@
     2.4  by (resolve_tac [appNil,appCons] 1);
     2.5  by (resolve_tac [appNil,appCons] 1);
     2.6  by (resolve_tac [appNil,appCons] 1);
     2.7 -prth (result());
     2.8 +result();
     2.9  
    2.10  Goal "app(?x, c:d:Nil, a:b:c:d:Nil)";
    2.11  by (REPEAT (resolve_tac [appNil,appCons] 1));
     3.1 --- a/src/FOLP/simp.ML	Tue Jul 21 00:56:19 2009 +0200
     3.2 +++ b/src/FOLP/simp.ML	Tue Jul 21 01:03:18 2009 +0200
     3.3 @@ -113,7 +113,7 @@
     3.4    let fun norm thm = 
     3.5        case lhs_of(concl_of thm) of
     3.6            Const(n,_)$_ => n
     3.7 -        | _ => (Display.prths normE_thms; error"No constant in lhs of a norm_thm")
     3.8 +        | _ => error "No constant in lhs of a norm_thm"
     3.9    in map norm normE_thms end;
    3.10  
    3.11  fun lhs_is_NORM(thm,i) = case lhs_of_eq i thm of
    3.12 @@ -122,7 +122,7 @@
    3.13  val refl_tac = resolve_tac refl_thms;
    3.14  
    3.15  fun find_res thms thm =
    3.16 -    let fun find [] = (Display.prths thms; error"Check Simp_Data")
    3.17 +    let fun find [] = error "Check Simp_Data"
    3.18            | find(th::thms) = thm RS th handle THM _ => find thms
    3.19      in find thms end;
    3.20  
    3.21 @@ -249,8 +249,8 @@
    3.22  fun insert_thm_warn th net = 
    3.23    Net.insert_term Thm.eq_thm_prop (concl_of th, th) net
    3.24    handle Net.INSERT => 
    3.25 -    (writeln"\nDuplicate rewrite or congruence rule:"; Display.print_thm th;
    3.26 -     net);
    3.27 +    (writeln ("Duplicate rewrite or congruence rule:\n" ^
    3.28 +        Display.string_of_thm_without_context th); net);
    3.29  
    3.30  val insert_thms = fold_rev insert_thm_warn;
    3.31  
    3.32 @@ -275,8 +275,8 @@
    3.33  fun delete_thm_warn th net = 
    3.34    Net.delete_term Thm.eq_thm_prop (concl_of th, th) net
    3.35    handle Net.DELETE => 
    3.36 -    (writeln"\nNo such rewrite or congruence rule:";  Display.print_thm th;
    3.37 -     net);
    3.38 +    (writeln ("No such rewrite or congruence rule:\n" ^
    3.39 +        Display.string_of_thm_without_context th); net);
    3.40  
    3.41  val delete_thms = fold_rev delete_thm_warn;
    3.42  
    3.43 @@ -290,9 +290,9 @@
    3.44  fun delrew(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}, thm) =
    3.45  let fun find((p as (th,ths))::ps',ps) =
    3.46            if Thm.eq_thm_prop(thm,th) then (ths,ps@ps') else find(ps',p::ps)
    3.47 -      | find([],simps') = (writeln"\nNo such rewrite or congruence rule:";
    3.48 -                           Display.print_thm thm;
    3.49 -                           ([],simps'))
    3.50 +      | find([],simps') =
    3.51 +          (writeln ("No such rewrite or congruence rule:\n" ^
    3.52 +              Display.string_of_thm_without_context thm); ([], simps'))
    3.53      val (thms,simps') = find(simps,[])
    3.54  in SS{auto_tac=auto_tac, congs=congs, cong_net=cong_net, mk_simps=mk_simps,
    3.55        simps = simps', simp_net = delete_thms thms simp_net }
    3.56 @@ -311,8 +311,9 @@
    3.57  fun dest_ss(SS{congs,simps,...}) = (congs, map #1 simps);
    3.58  
    3.59  fun print_ss(SS{congs,simps,...}) =
    3.60 -        (writeln"Congruences:"; Display.prths congs;
    3.61 -         writeln"Rewrite Rules:"; Display.prths (map #1 simps); ());
    3.62 +  writeln (cat_lines
    3.63 +   (["Congruences:"] @ map Display.string_of_thm_without_context congs @
    3.64 +    ["Rewrite Rules:"] @ map (Display.string_of_thm_without_context o #1) simps));
    3.65  
    3.66  
    3.67  (* Rewriting with conditionals *)
    3.68 @@ -435,7 +436,8 @@
    3.69          val rwrls = map mk_trans (List.concat(map mk_rew_rules thms));
    3.70          val anet' = List.foldr lhs_insert_thm anet rwrls
    3.71      in  if !tracing andalso not(null new_rws)
    3.72 -        then (writeln"Adding rewrites:";  Display.prths new_rws;  ())
    3.73 +        then writeln (cat_lines
    3.74 +          ("Adding rewrites:" :: map Display.string_of_thm_without_context new_rws))
    3.75          else ();
    3.76          (ss,thm,anet',anet::ats,cs) 
    3.77      end;
     4.1 --- a/src/HOL/Import/import.ML	Tue Jul 21 00:56:19 2009 +0200
     4.2 +++ b/src/HOL/Import/import.ML	Tue Jul 21 01:03:18 2009 +0200
     4.3 @@ -44,9 +44,9 @@
     4.4              val thm = equal_elim rew thm
     4.5              val prew = ProofKernel.rewrite_hol4_term prem thy
     4.6              val prem' = #2 (Logic.dest_equals (prop_of prew))
     4.7 -            val _ = message ("Import proved " ^ Display.string_of_thm thm)
     4.8 +            val _ = message ("Import proved " ^ Display.string_of_thm ctxt thm)
     4.9              val thm = ProofKernel.disambiguate_frees thm
    4.10 -            val _ = message ("Disambiguate: " ^ Display.string_of_thm thm)
    4.11 +            val _ = message ("Disambiguate: " ^ Display.string_of_thm ctxt thm)
    4.12          in
    4.13              case Shuffler.set_prop thy prem' [("",thm)] of
    4.14                  SOME (_,thm) =>
     5.1 --- a/src/HOL/Import/proof_kernel.ML	Tue Jul 21 00:56:19 2009 +0200
     5.2 +++ b/src/HOL/Import/proof_kernel.ML	Tue Jul 21 01:03:18 2009 +0200
     5.3 @@ -243,7 +243,7 @@
     5.4  
     5.5  val smart_string_of_thm = smart_string_of_cterm o cprop_of
     5.6  
     5.7 -fun prth th = writeln (PrintMode.setmp [] Display.string_of_thm th)
     5.8 +fun prth th = writeln (PrintMode.setmp [] Display.string_of_thm_without_context th)
     5.9  fun prc ct = writeln (PrintMode.setmp [] Display.string_of_cterm ct)
    5.10  fun prin t = writeln (PrintMode.setmp [] (fn () => Syntax.string_of_term_global (the_context ()) t) ());
    5.11  fun pth (HOLThm(ren,thm)) =
     6.1 --- a/src/HOL/Import/shuffler.ML	Tue Jul 21 00:56:19 2009 +0200
     6.2 +++ b/src/HOL/Import/shuffler.ML	Tue Jul 21 01:03:18 2009 +0200
     6.3 @@ -40,7 +40,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 Display.print_thm thms)
     6.8 +          List.app (writeln o Display.string_of_thm_global sign) 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 @@ -56,7 +56,7 @@
    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 [] Display.string_of_thm;
    6.17 +val string_of_thm = PrintMode.setmp [] Display.string_of_thm_without_context;
    6.18  val string_of_cterm = PrintMode.setmp [] Display.string_of_cterm;
    6.19  
    6.20  fun mk_meta_eq th =
    6.21 @@ -84,7 +84,7 @@
    6.22  
    6.23  fun print_shuffles thy =
    6.24    Pretty.writeln (Pretty.big_list "Shuffle theorems:"
    6.25 -    (map Display.pretty_thm (ShuffleData.get thy)))
    6.26 +    (map (Display.pretty_thm_global thy) (ShuffleData.get thy)))
    6.27  
    6.28  val weaken =
    6.29      let
     7.1 --- a/src/HOL/Nominal/nominal_thmdecls.ML	Tue Jul 21 00:56:19 2009 +0200
     7.2 +++ b/src/HOL/Nominal/nominal_thmdecls.ML	Tue Jul 21 01:03:18 2009 +0200
     7.3 @@ -156,7 +156,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 (Display.string_of_thm orig_thm ^ 
     7.8 +      error (Display.string_of_thm (Context.proof_of context) orig_thm ^ 
     7.9                 " does not comply with the form of an equivariance lemma (" ^ s ^").")
    7.10  
    7.11  
     8.1 --- a/src/HOL/Tools/TFL/casesplit.ML	Tue Jul 21 00:56:19 2009 +0200
     8.2 +++ b/src/HOL/Tools/TFL/casesplit.ML	Tue Jul 21 01:03:18 2009 +0200
     8.3 @@ -269,9 +269,9 @@
     8.4        fun split th =
     8.5            (case find_thms_split splitths 1 th of
     8.6               NONE =>
     8.7 -             (writeln "th:";
     8.8 -              Display.print_thm th; writeln "split ths:";
     8.9 -              Display.print_thms splitths; writeln "\n--";
    8.10 +             (writeln (cat_lines
    8.11 +              (["th:", Display.string_of_thm_without_context th, "split ths:"] @
    8.12 +                map Display.string_of_thm_without_context splitths @ ["\n--"]));
    8.13                error "splitto: cannot find variable to split on")
    8.14              | SOME v =>
    8.15               let
     9.1 --- a/src/HOL/Tools/TFL/rules.ML	Tue Jul 21 00:56:19 2009 +0200
     9.2 +++ b/src/HOL/Tools/TFL/rules.ML	Tue Jul 21 01:03:18 2009 +0200
     9.3 @@ -552,7 +552,7 @@
     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 Display.string_of_thm L));
     9.8 +  say (cat_lines (s :: map Display.string_of_thm_without_context L));
     9.9  
    9.10  fun print_cterms s L =
    9.11    say (cat_lines (s :: map Display.string_of_cterm L));
    9.12 @@ -677,7 +677,7 @@
    9.13               val cntxt = Simplifier.prems_of_ss ss
    9.14               val dummy = print_thms "cntxt:" cntxt
    9.15               val dummy = say "cong rule:"
    9.16 -             val dummy = say (Display.string_of_thm thm)
    9.17 +             val dummy = say (Display.string_of_thm_without_context thm)
    9.18               val dummy = thm_ref := (thm :: !thm_ref)
    9.19               val dummy = ss_ref := (ss :: !ss_ref)
    9.20               (* Unquantified eliminate *)
    10.1 --- a/src/HOL/Tools/TFL/tfl.ML	Tue Jul 21 00:56:19 2009 +0200
    10.2 +++ b/src/HOL/Tools/TFL/tfl.ML	Tue Jul 21 01:03:18 2009 +0200
    10.3 @@ -529,9 +529,8 @@
    10.4       val f = #lhs(S.dest_eq proto_def)
    10.5       val (extractants,TCl) = ListPair.unzip extracta
    10.6       val dummy = if !trace
    10.7 -                 then (writeln "Extractants = ";
    10.8 -                       Display.prths extractants;
    10.9 -                       ())
   10.10 +                 then writeln (cat_lines ("Extractants =" ::
   10.11 +                  map (Display.string_of_thm_global thy) extractants))
   10.12                   else ()
   10.13       val TCs = List.foldr (gen_union (op aconv)) [] TCl
   10.14       val full_rqt = WFR::TCs
   10.15 @@ -551,8 +550,9 @@
   10.16         |> PureThy.add_defs false
   10.17              [Thm.no_attributes (Binding.name (fid ^ "_def"), defn)]
   10.18       val def = Thm.freezeT def0;
   10.19 -     val dummy = if !trace then writeln ("DEF = " ^ Display.string_of_thm def)
   10.20 -                           else ()
   10.21 +     val dummy =
   10.22 +       if !trace then writeln ("DEF = " ^ Display.string_of_thm_global theory def)
   10.23 +       else ()
   10.24       (* val fconst = #lhs(S.dest_eq(concl def))  *)
   10.25       val tych = Thry.typecheck theory
   10.26       val full_rqt_prop = map (Dcterm.mk_prop o tych) full_rqt
   10.27 @@ -560,7 +560,7 @@
   10.28       val baz = R.DISCH_ALL
   10.29                   (fold_rev R.DISCH full_rqt_prop
   10.30                    (R.LIST_CONJ extractants))
   10.31 -     val dum = if !trace then writeln ("baz = " ^ Display.string_of_thm baz)
   10.32 +     val dum = if !trace then writeln ("baz = " ^ Display.string_of_thm_global theory baz)
   10.33                             else ()
   10.34       val f_free = Free (fid, fastype_of f)  (*'cos f is a Const*)
   10.35       val SV' = map tych SV;
   10.36 @@ -909,7 +909,7 @@
   10.37  
   10.38  
   10.39  fun trace_thms s L =
   10.40 -  if !trace then writeln (cat_lines (s :: map Display.string_of_thm L))
   10.41 +  if !trace then writeln (cat_lines (s :: map Display.string_of_thm_without_context L))
   10.42    else ();
   10.43  
   10.44  fun trace_cterms s L =
    11.1 --- a/src/HOL/Tools/atp_minimal.ML	Tue Jul 21 00:56:19 2009 +0200
    11.2 +++ b/src/HOL/Tools/atp_minimal.ML	Tue Jul 21 01:03:18 2009 +0200
    11.3 @@ -125,7 +125,8 @@
    11.4        println ("Minimize called with " ^ length_string name_thms_pairs ^ " theorems, prover: "
    11.5          ^ prover_name ^ ", time limit: " ^ Int.toString time_limit ^ " seconds")
    11.6      val _ = debug_fn (fn () => app (fn (n, tl) =>
    11.7 -        (debug n; app (fn t => debug ("  " ^ Display.string_of_thm t)) tl)) name_thms_pairs)
    11.8 +        (debug n; app (fn t =>
    11.9 +          debug ("  " ^ Display.string_of_thm (Proof.context_of state) t)) tl)) name_thms_pairs)
   11.10      val test_thms_fun = sh_test_thms prover prover_name time_limit 1 state
   11.11      fun test_thms filtered thms =
   11.12        case test_thms_fun filtered thms of (Success _, _) => true | _ => false
    12.1 --- a/src/HOL/Tools/atp_wrapper.ML	Tue Jul 21 00:56:19 2009 +0200
    12.2 +++ b/src/HOL/Tools/atp_wrapper.ML	Tue Jul 21 01:03:18 2009 +0200
    12.3 @@ -62,7 +62,7 @@
    12.4      val goal_cls = #1 (ResAxioms.neg_conjecture_clauses th subgoalno)
    12.5        handle THM ("assume: variables", _, _) =>
    12.6          error "Sledgehammer: Goal contains type variables (TVars)"
    12.7 -    val _ = app (fn th => Output.debug (fn _ => Display.string_of_thm th)) goal_cls
    12.8 +    val _ = app (fn th => Output.debug (fn _ => Display.string_of_thm ctxt th)) goal_cls
    12.9      val the_filtered_clauses =
   12.10        case filtered_clauses of
   12.11            NONE => relevance_filter goal goal_cls
    13.1 --- a/src/HOL/Tools/choice_specification.ML	Tue Jul 21 00:56:19 2009 +0200
    13.2 +++ b/src/HOL/Tools/choice_specification.ML	Tue Jul 21 01:03:18 2009 +0200
    13.3 @@ -183,7 +183,7 @@
    13.4                          fun add_final (arg as (thy, thm)) =
    13.5                              if name = ""
    13.6                              then arg |> Library.swap
    13.7 -                            else (writeln ("  " ^ name ^ ": " ^ (Display.string_of_thm thm));
    13.8 +                            else (writeln ("  " ^ name ^ ": " ^ Display.string_of_thm_global thy thm);
    13.9                                    PureThy.store_thm (Binding.name name, thm) thy)
   13.10                      in
   13.11                          args |> apsnd (remove_alls frees)
    14.1 --- a/src/HOL/Tools/inductive.ML	Tue Jul 21 00:56:19 2009 +0200
    14.2 +++ b/src/HOL/Tools/inductive.ML	Tue Jul 21 01:03:18 2009 +0200
    14.3 @@ -140,7 +140,7 @@
    14.4      val space = Consts.space_of (ProofContext.consts_of ctxt);
    14.5    in
    14.6      [Pretty.strs ("(co)inductives:" :: map #1 (NameSpace.extern_table (space, tab))),
    14.7 -     Pretty.big_list "monotonicity rules:" (map (ProofContext.pretty_thm ctxt) monos)]
    14.8 +     Pretty.big_list "monotonicity rules:" (map (Display.pretty_thm ctxt) monos)]
    14.9      |> Pretty.chunks |> Pretty.writeln
   14.10    end;
   14.11  
   14.12 @@ -179,7 +179,8 @@
   14.13        [dest_less_concl (Seq.hd (REPEAT (FIRSTGOAL
   14.14           (resolve_tac [le_funI, le_boolI'])) thm))]
   14.15      | _ => [thm]
   14.16 -  end handle THM _ => error ("Bad monotonicity theorem:\n" ^ Display.string_of_thm thm);
   14.17 +  end handle THM _ =>
   14.18 +    error ("Bad monotonicity theorem:\n" ^ Display.string_of_thm_without_context thm);
   14.19  
   14.20  val mono_add = Thm.declaration_attribute (map_monos o fold Thm.add_thm o mk_mono);
   14.21  val mono_del = Thm.declaration_attribute (map_monos o fold Thm.del_thm o mk_mono);
    15.1 --- a/src/HOL/Tools/inductive_codegen.ML	Tue Jul 21 00:56:19 2009 +0200
    15.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Tue Jul 21 01:03:18 2009 +0200
    15.3 @@ -39,7 +39,7 @@
    15.4  
    15.5  
    15.6  fun warn thm = warning ("InductiveCodegen: Not a proper clause:\n" ^
    15.7 -  Display.string_of_thm thm);
    15.8 +  Display.string_of_thm_without_context thm);
    15.9  
   15.10  fun add_node (g, x) = Graph.new_node (x, ()) g handle Graph.DUP _ => g;
   15.11  
    16.1 --- a/src/HOL/Tools/inductive_realizer.ML	Tue Jul 21 00:56:19 2009 +0200
    16.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Tue Jul 21 01:03:18 2009 +0200
    16.3 @@ -19,7 +19,7 @@
    16.4    (case Proofterm.fold_proof_atoms false (fn PThm (_, ((name, _, _), _)) => cons name | _ => I)
    16.5        [Thm.proof_of thm] [] of
    16.6      [name] => name
    16.7 -  | _ => error ("name_of_thm: bad proof of theorem\n" ^ Display.string_of_thm thm));
    16.8 +  | _ => error ("name_of_thm: bad proof of theorem\n" ^ Display.string_of_thm_without_context thm));
    16.9  
   16.10  val all_simps = map (symmetric o mk_meta_eq) (thms "HOL.all_simps");
   16.11  
    17.1 --- a/src/HOL/Tools/lin_arith.ML	Tue Jul 21 00:56:19 2009 +0200
    17.2 +++ b/src/HOL/Tools/lin_arith.ML	Tue Jul 21 01:03:18 2009 +0200
    17.3 @@ -286,7 +286,7 @@
    17.4  
    17.5  (* checks if splitting with 'thm' is implemented                             *)
    17.6  
    17.7 -fun is_split_thm (thm : thm) : bool =
    17.8 +fun is_split_thm thm =
    17.9    case concl_of thm of _ $ (_ $ (_ $ lhs) $ _) => (
   17.10      (* Trueprop $ ((op =) $ (?P $ lhs) $ rhs) *)
   17.11      case head_of lhs of
   17.12 @@ -298,10 +298,10 @@
   17.13                                      "Divides.div_class.mod",
   17.14                                      "Divides.div_class.div"] a
   17.15      | _            => (warning ("Lin. Arith.: wrong format for split rule " ^
   17.16 -                                 Display.string_of_thm thm);
   17.17 +                                 Display.string_of_thm_without_context thm);
   17.18                         false))
   17.19    | _ => (warning ("Lin. Arith.: wrong format for split rule " ^
   17.20 -                   Display.string_of_thm thm);
   17.21 +                   Display.string_of_thm_without_context thm);
   17.22            false);
   17.23  
   17.24  (* substitute new for occurrences of old in a term, incrementing bound       *)
    18.1 --- a/src/HOL/Tools/meson.ML	Tue Jul 21 00:56:19 2009 +0200
    18.2 +++ b/src/HOL/Tools/meson.ML	Tue Jul 21 01:03:18 2009 +0200
    18.3 @@ -127,10 +127,10 @@
    18.4  fun forward_res nf st =
    18.5    let fun forward_tacf [prem] = rtac (nf prem) 1
    18.6          | forward_tacf prems =
    18.7 -            error ("Bad proof state in forward_res, please inform lcp@cl.cam.ac.uk:\n" ^
    18.8 -                   Display.string_of_thm st ^
    18.9 -                   "\nPremises:\n" ^
   18.10 -                   ML_Syntax.print_list Display.string_of_thm prems)
   18.11 +            error (cat_lines
   18.12 +              ("Bad proof state in forward_res, please inform lcp@cl.cam.ac.uk:" ::
   18.13 +                Display.string_of_thm_without_context st ::
   18.14 +                "Premises:" :: map Display.string_of_thm_without_context prems))
   18.15    in
   18.16      case Seq.pull (ALLGOALS (METAHYPS forward_tacf) st)
   18.17      of SOME(th,_) => th
   18.18 @@ -342,7 +342,7 @@
   18.19        and cnf_nil th = cnf_aux (th,[])
   18.20        val cls = 
   18.21  	    if too_many_clauses (SOME ctxt) (concl_of th)
   18.22 -	    then (warning ("cnf is ignoring: " ^ Display.string_of_thm th); ths)
   18.23 +	    then (warning ("cnf is ignoring: " ^ Display.string_of_thm ctxt th); ths)
   18.24  	    else cnf_aux (th,ths)
   18.25    in  (cls, !ctxtr)  end;
   18.26  
   18.27 @@ -545,7 +545,7 @@
   18.28    | skolemize_nnf_list (th::ths) = 
   18.29        skolemize th :: skolemize_nnf_list ths
   18.30        handle THM _ => (*RS can fail if Unify.search_bound is too small*)
   18.31 -       (warning ("Failed to Skolemize " ^ Display.string_of_thm th);
   18.32 +       (warning ("Failed to Skolemize " ^ Display.string_of_thm_without_context th);
   18.33          skolemize_nnf_list ths);
   18.34  
   18.35  fun add_clauses (th,cls) =
   18.36 @@ -628,19 +628,17 @@
   18.37      ITER_DEEPEN (has_fewer_prems 1) (prolog_step_tac' horns);
   18.38  
   18.39  fun iter_deepen_meson_tac ths = MESON make_clauses
   18.40 - (fn cls =>
   18.41 -      case (gocls (cls@ths)) of
   18.42 -           [] => no_tac  (*no goal clauses*)
   18.43 -         | goes =>
   18.44 -             let val horns = make_horns (cls@ths)
   18.45 -                 val _ =
   18.46 -                     Output.debug (fn () => ("meson method called:\n" ^
   18.47 -                                  ML_Syntax.print_list Display.string_of_thm (cls@ths) ^
   18.48 -                                  "\nclauses:\n" ^
   18.49 -                                  ML_Syntax.print_list Display.string_of_thm horns))
   18.50 -             in THEN_ITER_DEEPEN (resolve_tac goes 1) (has_fewer_prems 1) (prolog_step_tac' horns)
   18.51 -             end
   18.52 - );
   18.53 +  (fn cls =>
   18.54 +    (case (gocls (cls @ ths)) of
   18.55 +      [] => no_tac  (*no goal clauses*)
   18.56 +    | goes =>
   18.57 +        let
   18.58 +          val horns = make_horns (cls @ ths)
   18.59 +          val _ = Output.debug (fn () =>
   18.60 +            cat_lines ("meson method called:" ::
   18.61 +              map Display.string_of_thm_without_context (cls @ ths) @
   18.62 +              ["clauses:"] @ map Display.string_of_thm_without_context horns))
   18.63 +        in THEN_ITER_DEEPEN (resolve_tac goes 1) (has_fewer_prems 1) (prolog_step_tac' horns) end));
   18.64  
   18.65  fun meson_claset_tac ths cs =
   18.66    SELECT_GOAL (TRY (safe_tac cs) THEN TRYALL (iter_deepen_meson_tac ths));
    19.1 --- a/src/HOL/Tools/metis_tools.ML	Tue Jul 21 00:56:19 2009 +0200
    19.2 +++ b/src/HOL/Tools/metis_tools.ML	Tue Jul 21 01:03:18 2009 +0200
    19.3 @@ -270,7 +270,7 @@
    19.4    fun print_thpair (fth,th) =
    19.5      (Output.debug (fn () => "=============================================");
    19.6       Output.debug (fn () => "Metis: " ^ Metis.Thm.toString fth);
    19.7 -     Output.debug (fn () => "Isabelle: " ^ Display.string_of_thm th));
    19.8 +     Output.debug (fn () => "Isabelle: " ^ Display.string_of_thm_without_context th));
    19.9  
   19.10    fun lookth thpairs (fth : Metis.Thm.thm) =
   19.11      valOf (AList.lookup (uncurry Metis.Thm.equal) thpairs fth)
   19.12 @@ -310,7 +310,7 @@
   19.13                in  SOME (cterm_of thy (Var v), t)  end
   19.14                handle Option =>
   19.15                    (Output.debug (fn() => "List.find failed for the variable " ^ x ^
   19.16 -                                         " in " ^ Display.string_of_thm i_th);
   19.17 +                                         " in " ^ Display.string_of_thm ctxt i_th);
   19.18                     NONE)
   19.19          fun remove_typeinst (a, t) =
   19.20                case Recon.strip_prefix ResClause.schematic_var_prefix a of
   19.21 @@ -318,7 +318,7 @@
   19.22                  | NONE   => case Recon.strip_prefix ResClause.tvar_prefix a of
   19.23                    SOME _ => NONE          (*type instantiations are forbidden!*)
   19.24                  | NONE   => SOME (a,t)    (*internal Metis var?*)
   19.25 -        val _ = Output.debug (fn () => "  isa th: " ^ Display.string_of_thm i_th)
   19.26 +        val _ = Output.debug (fn () => "  isa th: " ^ Display.string_of_thm ctxt i_th)
   19.27          val substs = List.mapPartial remove_typeinst (Metis.Subst.toList fsubst)
   19.28          val (vars,rawtms) = ListPair.unzip (List.mapPartial subst_translation substs)
   19.29          val tms = infer_types ctxt rawtms;
   19.30 @@ -350,8 +350,8 @@
   19.31      let
   19.32        val thy = ProofContext.theory_of ctxt
   19.33        val i_th1 = lookth thpairs th1 and i_th2 = lookth thpairs th2
   19.34 -      val _ = Output.debug (fn () => "  isa th1 (pos): " ^ Display.string_of_thm i_th1)
   19.35 -      val _ = Output.debug (fn () => "  isa th2 (neg): " ^ Display.string_of_thm i_th2)
   19.36 +      val _ = Output.debug (fn () => "  isa th1 (pos): " ^ Display.string_of_thm ctxt i_th1)
   19.37 +      val _ = Output.debug (fn () => "  isa th2 (neg): " ^ Display.string_of_thm ctxt i_th2)
   19.38      in
   19.39        if is_TrueI i_th1 then i_th2 (*Trivial cases where one operand is type info*)
   19.40        else if is_TrueI i_th2 then i_th1
   19.41 @@ -428,7 +428,7 @@
   19.42          val _ = Output.debug (fn () => "located term: " ^ Syntax.string_of_term ctxt tm_subst)
   19.43          val imax = maxidx_of_term (i_tm $ tm_abs $ tm_subst)  (*ill typed but gives right max*)
   19.44          val subst' = incr_indexes (imax+1) (if pos then subst_em else ssubst_em)
   19.45 -        val _ = Output.debug (fn () => "subst' " ^ Display.string_of_thm subst')
   19.46 +        val _ = Output.debug (fn () => "subst' " ^ Display.string_of_thm ctxt subst')
   19.47          val eq_terms = map (pairself (cterm_of thy))
   19.48                             (ListPair.zip (OldTerm.term_vars (prop_of subst'), [tm_abs, tm_subst, i_tm]))
   19.49      in  cterm_instantiate eq_terms subst'  end;
   19.50 @@ -456,7 +456,7 @@
   19.51              val _ = Output.debug (fn () => "METIS THM: " ^ Metis.Thm.toString fol_th)
   19.52              val _ = Output.debug (fn () => "INFERENCE: " ^ Metis.Proof.inferenceToString inf)
   19.53              val th = Meson.flexflex_first_order (step ctxt isFO thpairs (fol_th, inf))
   19.54 -            val _ = Output.debug (fn () => "ISABELLE THM: " ^ Display.string_of_thm th)
   19.55 +            val _ = Output.debug (fn () => "ISABELLE THM: " ^ Display.string_of_thm ctxt th)
   19.56              val _ = Output.debug (fn () => "=============================================")
   19.57              val n_metis_lits = length (filter real_literal (Metis.LiteralSet.toList (Metis.Thm.clause fol_th)))
   19.58          in
   19.59 @@ -576,9 +576,9 @@
   19.60          val th_cls_pairs = map (fn th => (Thm.get_name_hint th, ResAxioms.cnf_axiom thy th)) ths0
   19.61          val ths = List.concat (map #2 th_cls_pairs)
   19.62          val _ = Output.debug (fn () => "FOL_SOLVE: CONJECTURE CLAUSES")
   19.63 -        val _ = app (fn th => Output.debug (fn () => Display.string_of_thm th)) cls
   19.64 +        val _ = app (fn th => Output.debug (fn () => Display.string_of_thm ctxt th)) cls
   19.65          val _ = Output.debug (fn () => "THEOREM CLAUSES")
   19.66 -        val _ = app (fn th => Output.debug (fn () => Display.string_of_thm th)) ths
   19.67 +        val _ = app (fn th => Output.debug (fn () => Display.string_of_thm ctxt th)) ths
   19.68          val {isFO,axioms,tfrees} = build_map mode ctxt cls ths
   19.69          val _ = if null tfrees then ()
   19.70                  else (Output.debug (fn () => "TFREE CLAUSES");
   19.71 @@ -604,14 +604,14 @@
   19.72                    val result = translate isFO ctxt' axioms proof
   19.73                    and used = List.mapPartial (used_axioms axioms) proof
   19.74                    val _ = Output.debug (fn () => "METIS COMPLETED...clauses actually used:")
   19.75 -	          val _ = app (fn th => Output.debug (fn () => Display.string_of_thm th)) used
   19.76 +	          val _ = app (fn th => Output.debug (fn () => Display.string_of_thm ctxt th)) used
   19.77  	          val unused = filter (fn (a,cls) => not (common_thm used cls)) th_cls_pairs
   19.78                in
   19.79                    if null unused then ()
   19.80                    else warning ("Metis: unused theorems " ^ commas_quote (map #1 unused));
   19.81                    case result of
   19.82                        (_,ith)::_ => 
   19.83 -                          (Output.debug (fn () => "success: " ^ Display.string_of_thm ith); 
   19.84 +                          (Output.debug (fn () => "success: " ^ Display.string_of_thm ctxt ith); 
   19.85                             [ith])
   19.86                      | _ => (Output.debug (fn () => "Metis: no result"); 
   19.87                              [])
   19.88 @@ -623,7 +623,7 @@
   19.89  
   19.90    fun metis_general_tac mode ctxt ths i st0 =
   19.91      let val _ = Output.debug (fn () =>
   19.92 -          "Metis called with theorems " ^ cat_lines (map Display.string_of_thm ths))
   19.93 +          "Metis called with theorems " ^ cat_lines (map (Display.string_of_thm ctxt) ths))
   19.94      in
   19.95         if exists_type ResAxioms.type_has_empty_sort (prop_of st0)  
   19.96         then (warning "Proof state contains the empty sort"; Seq.empty)
    20.1 --- a/src/HOL/Tools/recdef.ML	Tue Jul 21 00:56:19 2009 +0200
    20.2 +++ b/src/HOL/Tools/recdef.ML	Tue Jul 21 01:03:18 2009 +0200
    20.3 @@ -48,9 +48,9 @@
    20.4  fun map_wfs f = map_hints (fn (simps, congs, wfs) => (simps, congs, f wfs));
    20.5  
    20.6  fun pretty_hints ({simps, congs, wfs}: hints) =
    20.7 - [Pretty.big_list "recdef simp hints:" (map Display.pretty_thm simps),
    20.8 -  Pretty.big_list "recdef cong hints:" (map Display.pretty_thm (map snd congs)),
    20.9 -  Pretty.big_list "recdef wf hints:" (map Display.pretty_thm wfs)];
   20.10 + [Pretty.big_list "recdef simp hints:" (map Display.pretty_thm_without_context simps),
   20.11 +  Pretty.big_list "recdef cong hints:" (map Display.pretty_thm_without_context (map snd congs)),
   20.12 +  Pretty.big_list "recdef wf hints:" (map Display.pretty_thm_without_context wfs)];
   20.13  
   20.14  
   20.15  (* congruence rules *)
    21.1 --- a/src/HOL/Tools/record.ML	Tue Jul 21 00:56:19 2009 +0200
    21.2 +++ b/src/HOL/Tools/record.ML	Tue Jul 21 01:03:18 2009 +0200
    21.3 @@ -105,7 +105,7 @@
    21.4  (* messages *)
    21.5  
    21.6  fun trace_thm str thm =
    21.7 -    tracing (str ^ (Pretty.string_of (Display.pretty_thm thm)));
    21.8 +    tracing (str ^ (Pretty.string_of (Display.pretty_thm_without_context thm)));
    21.9  
   21.10  fun trace_thms str thms =
   21.11      (tracing str; map (trace_thm "") thms);
    22.1 --- a/src/HOL/Tools/res_atp.ML	Tue Jul 21 00:56:19 2009 +0200
    22.2 +++ b/src/HOL/Tools/res_atp.ML	Tue Jul 21 01:03:18 2009 +0200
    22.3 @@ -401,8 +401,9 @@
    22.4          (List.foldl add_single_names (List.foldl add_multi_names [] mults) singles)
    22.5    end;
    22.6  
    22.7 -fun check_named ("",th) = (warning ("No name for theorem " ^ Display.string_of_thm th); false)
    22.8 -  | check_named (_,th) = true;
    22.9 +fun check_named ("", th) =
   22.10 +      (warning ("No name for theorem " ^ Display.string_of_thm_without_context th); false)
   22.11 +  | check_named (_, th) = true;
   22.12  
   22.13  (* get lemmas from claset, simpset, atpset and extra supplied rules *)
   22.14  fun get_clasimp_atp_lemmas ctxt =
   22.15 @@ -538,7 +539,7 @@
   22.16      val extra_cls = white_cls @ extra_cls
   22.17      val axcls = white_cls @ axcls
   22.18      val ccls = subtract_cls goal_cls extra_cls
   22.19 -    val _ = app (fn th => Output.debug (fn _ => Display.string_of_thm th)) ccls
   22.20 +    val _ = app (fn th => Output.debug (fn _ => Display.string_of_thm_global thy th)) ccls
   22.21      val ccltms = map prop_of ccls
   22.22      and axtms = map (prop_of o #1) extra_cls
   22.23      val subs = tfree_classes_of_terms ccltms
    23.1 --- a/src/HOL/Tools/res_axioms.ML	Tue Jul 21 00:56:19 2009 +0200
    23.2 +++ b/src/HOL/Tools/res_axioms.ML	Tue Jul 21 01:03:18 2009 +0200
    23.3 @@ -227,8 +227,9 @@
    23.4          val eqth = combinators_aux (cprop_of th)
    23.5      in  equal_elim eqth th   end
    23.6      handle THM (msg,_,_) =>
    23.7 -      (warning ("Error in the combinator translation of " ^ Display.string_of_thm th);
    23.8 -       warning ("  Exception message: " ^ msg);
    23.9 +      (warning (cat_lines
   23.10 +        ["Error in the combinator translation of " ^ Display.string_of_thm_without_context th,
   23.11 +          "  Exception message: " ^ msg]);
   23.12         TrueI);  (*A type variable of sort {} will cause make abstraction fail.*)
   23.13  
   23.14  (*cterms are used throughout for efficiency*)
   23.15 @@ -280,7 +281,7 @@
   23.16  fun assert_lambda_free ths msg =
   23.17    case filter (not o lambda_free o prop_of) ths of
   23.18        [] => ()
   23.19 -    | ths' => error (msg ^ "\n" ^ cat_lines (map Display.string_of_thm ths'));
   23.20 +    | ths' => error (cat_lines (msg :: map Display.string_of_thm_without_context ths'));
   23.21  
   23.22  
   23.23  (*** Blacklisting (duplicated in ResAtp?) ***)
   23.24 @@ -336,7 +337,7 @@
   23.25  
   23.26  fun name_or_string th =
   23.27    if Thm.has_name_hint th then Thm.get_name_hint th
   23.28 -  else Display.string_of_thm th;
   23.29 +  else Display.string_of_thm_without_context th;
   23.30  
   23.31  (*Skolemize a named theorem, with Skolem functions as additional premises.*)
   23.32  fun skolem_thm (s, th) =
    24.1 --- a/src/HOL/Tools/res_reconstruct.ML	Tue Jul 21 00:56:19 2009 +0200
    24.2 +++ b/src/HOL/Tools/res_reconstruct.ML	Tue Jul 21 01:03:18 2009 +0200
    24.3 @@ -31,7 +31,7 @@
    24.4  fun trace s = if !Output.debugging then File.append (File.tmp_path trace_path) s
    24.5                else ();
    24.6  
    24.7 -val string_of_thm = PrintMode.setmp [] Display.string_of_thm;
    24.8 +fun string_of_thm ctxt = PrintMode.setmp [] (Display.string_of_thm ctxt);
    24.9  
   24.10  (*For generating structured proofs: keep every nth proof line*)
   24.11  val (modulus, modulus_setup) = Attrib.config_int "sledgehammer_modulus" 1;
   24.12 @@ -445,8 +445,9 @@
   24.13        val (ccls,fixes) = ResAxioms.neg_conjecture_clauses th sgno
   24.14        val _ = trace (Int.toString (length ccls) ^ " conjecture clauses\n")
   24.15        val ccls = map forall_intr_vars ccls
   24.16 -      val _ = if !Output.debugging then app (fn th => trace ("\nccl: " ^ string_of_thm th)) ccls
   24.17 -              else ()
   24.18 +      val _ =
   24.19 +        if !Output.debugging then app (fn th => trace ("\nccl: " ^ string_of_thm ctxt th)) ccls
   24.20 +        else ()
   24.21        val ilines = isar_lines ctxt (map prop_of ccls) (stringify_deps thm_names [] lines)
   24.22        val _ = trace "\ndecode_tstp_file: finishing\n"
   24.23    in
    25.1 --- a/src/HOL/Tools/sat_funcs.ML	Tue Jul 21 00:56:19 2009 +0200
    25.2 +++ b/src/HOL/Tools/sat_funcs.ML	Tue Jul 21 01:03:18 2009 +0200
    25.3 @@ -119,7 +119,7 @@
    25.4  (* (Thm.thm * (int * Thm.cterm) list) list -> Thm.thm * (int * Thm.cterm) list *)
    25.5  
    25.6  fun resolve_raw_clauses [] =
    25.7 -	raise THM ("Proof reconstruction failed (empty list of resolvents)!", 0, [])
    25.8 +      raise THM ("Proof reconstruction failed (empty list of resolvents)!", 0, [])
    25.9    | resolve_raw_clauses (c::cs) =
   25.10  	let
   25.11  		(* merges two sorted lists wrt. 'lit_ord', suppressing duplicates *)
   25.12 @@ -134,9 +134,9 @@
   25.13  		(* find out which two hyps are used in the resolution *)
   25.14  		(* (int * Thm.cterm) list * (int * Thm.cterm) list -> (int * Thm.cterm) list -> bool * Thm.cterm * Thm.cterm * (int * Thm.cterm) list *)
   25.15  		fun find_res_hyps ([], _) _ =
   25.16 -			raise THM ("Proof reconstruction failed (no literal for resolution)!", 0, [])
   25.17 +          raise THM ("Proof reconstruction failed (no literal for resolution)!", 0, [])
   25.18  		  | find_res_hyps (_, []) _ =
   25.19 -			raise THM ("Proof reconstruction failed (no literal for resolution)!", 0, [])
   25.20 +          raise THM ("Proof reconstruction failed (no literal for resolution)!", 0, [])
   25.21  		  | find_res_hyps (h1 :: hyps1, h2 :: hyps2) acc =
   25.22  			(case (lit_ord o pairself fst) (h1, h2) of
   25.23  			  LESS  => find_res_hyps (hyps1, h2 :: hyps2) (h1 :: acc)
   25.24 @@ -154,9 +154,12 @@
   25.25  		(* Thm.thm * (int * Thm.cterm) list -> Thm.thm * (int * Thm.cterm) list -> Thm.thm * (int * Thm.cterm) list *)
   25.26  		fun resolution (c1, hyps1) (c2, hyps2) =
   25.27  		let
   25.28 -			val _ = if !trace_sat then
   25.29 -					tracing ("Resolving clause: " ^ Display.string_of_thm c1 ^ " (hyps: " ^ ML_Syntax.print_list (Syntax.string_of_term_global (theory_of_thm c1)) (#hyps (rep_thm c1))
   25.30 -						^ ")\nwith clause: " ^ Display.string_of_thm c2 ^ " (hyps: " ^ ML_Syntax.print_list (Syntax.string_of_term_global (theory_of_thm c2)) (#hyps (rep_thm c2)) ^ ")")
   25.31 +			val _ =
   25.32 +			  if ! trace_sat then
   25.33 +					tracing ("Resolving clause: " ^ Display.string_of_thm_without_context c1 ^
   25.34 +					  " (hyps: " ^ ML_Syntax.print_list (Syntax.string_of_term_global (theory_of_thm c1)) (#hyps (rep_thm c1))
   25.35 +						^ ")\nwith clause: " ^ Display.string_of_thm_without_context c2 ^
   25.36 +						" (hyps: " ^ ML_Syntax.print_list (Syntax.string_of_term_global (theory_of_thm c2)) (#hyps (rep_thm c2)) ^ ")")
   25.37  				else ()
   25.38  
   25.39  			(* the two literals used for resolution *)
   25.40 @@ -172,8 +175,9 @@
   25.41  					Thm.instantiate ([], [(cP, cLit)]) resolution_thm
   25.42  				end
   25.43  
   25.44 -			val _ = if !trace_sat then
   25.45 -					tracing ("Resolution theorem: " ^ Display.string_of_thm res_thm)
   25.46 +			val _ =
   25.47 +			  if !trace_sat then
   25.48 +					tracing ("Resolution theorem: " ^ Display.string_of_thm_without_context res_thm)
   25.49  				else ()
   25.50  
   25.51  			(* Gamma1, Gamma2 |- False *)
   25.52 @@ -181,8 +185,11 @@
   25.53  				(Thm.implies_elim res_thm (if hyp1_is_neg then c2' else c1'))
   25.54  				(if hyp1_is_neg then c1' else c2')
   25.55  
   25.56 -			val _ = if !trace_sat then
   25.57 -					tracing ("Resulting clause: " ^ Display.string_of_thm c_new ^ " (hyps: " ^ ML_Syntax.print_list (Syntax.string_of_term_global (theory_of_thm c_new)) (#hyps (rep_thm c_new)) ^ ")")
   25.58 +			val _ =
   25.59 +			  if !trace_sat then
   25.60 +					tracing ("Resulting clause: " ^ Display.string_of_thm_without_context c_new ^
   25.61 +					  " (hyps: " ^ ML_Syntax.print_list
   25.62 +					      (Syntax.string_of_term_global (theory_of_thm c_new)) (#hyps (rep_thm c_new)) ^ ")")
   25.63  				else ()
   25.64  			val _ = inc counter
   25.65  		in
    26.1 --- a/src/HOL/ex/predicate_compile.ML	Tue Jul 21 00:56:19 2009 +0200
    26.2 +++ b/src/HOL/ex/predicate_compile.ML	Tue Jul 21 01:03:18 2009 +0200
    26.3 @@ -236,11 +236,11 @@
    26.4        val _ = writeln ("predicate: " ^ pred)
    26.5        val _ = writeln ("number of parameters: " ^ string_of_int (nparams_of thy pred))
    26.6        val _ = writeln ("introrules: ")
    26.7 -      val _ = fold (fn thm => fn u =>  writeln (Display.string_of_thm thm))
    26.8 +      val _ = fold (fn thm => fn u => writeln (Display.string_of_thm_global thy thm))
    26.9          (rev (intros_of thy pred)) ()
   26.10      in
   26.11        if (has_elim thy pred) then
   26.12 -        writeln ("elimrule: " ^ Display.string_of_thm (the_elim_of thy pred))
   26.13 +        writeln ("elimrule: " ^ Display.string_of_thm_global thy (the_elim_of thy pred))
   26.14        else
   26.15          writeln ("no elimrule defined")
   26.16      end
    27.1 --- a/src/Provers/Arith/fast_lin_arith.ML	Tue Jul 21 00:56:19 2009 +0200
    27.2 +++ b/src/Provers/Arith/fast_lin_arith.ML	Tue Jul 21 01:03:18 2009 +0200
    27.3 @@ -417,8 +417,8 @@
    27.4  (* Translate back a proof.                                                   *)
    27.5  (* ------------------------------------------------------------------------- *)
    27.6  
    27.7 -fun trace_thm msg th =
    27.8 -  (if !trace then (tracing msg; tracing (Display.string_of_thm th)) else (); th);
    27.9 +fun trace_thm ctxt msg th =
   27.10 +  (if !trace then (tracing msg; tracing (Display.string_of_thm ctxt th)) else (); th);
   27.11  
   27.12  fun trace_term ctxt msg t =
   27.13    (if !trace then tracing (cat_lines [msg, Syntax.string_of_term ctxt t]) else (); t)
   27.14 @@ -472,7 +472,7 @@
   27.15              NONE =>
   27.16                (the (try_add ([thm2] RL inj_thms) thm1)
   27.17                  handle Option =>
   27.18 -                  (trace_thm "" thm1; trace_thm "" thm2;
   27.19 +                  (trace_thm ctxt "" thm1; trace_thm ctxt "" thm2;
   27.20                     sys_error "Linear arithmetic: failed to add thms"))
   27.21            | SOME thm => thm)
   27.22        | SOME thm => thm);
   27.23 @@ -511,24 +511,25 @@
   27.24        else mult n thm;
   27.25  
   27.26      fun simp thm =
   27.27 -      let val thm' = trace_thm "Simplified:" (full_simplify simpset' thm)
   27.28 +      let val thm' = trace_thm ctxt "Simplified:" (full_simplify simpset' thm)
   27.29        in if LA_Logic.is_False thm' then raise FalseE thm' else thm' end;
   27.30  
   27.31 -    fun mk (Asm i) = trace_thm ("Asm " ^ string_of_int i) (nth asms i)
   27.32 -      | mk (Nat i) = trace_thm ("Nat " ^ string_of_int i) (LA_Logic.mk_nat_thm thy (nth atoms i))
   27.33 -      | mk (LessD j)            = trace_thm "L" (hd ([mk j] RL lessD))
   27.34 -      | mk (NotLeD j)           = trace_thm "NLe" (mk j RS LA_Logic.not_leD)
   27.35 -      | mk (NotLeDD j)          = trace_thm "NLeD" (hd ([mk j RS LA_Logic.not_leD] RL lessD))
   27.36 -      | mk (NotLessD j)         = trace_thm "NL" (mk j RS LA_Logic.not_lessD)
   27.37 -      | mk (Added (j1, j2))     = simp (trace_thm "+" (add_thms (mk j1) (mk j2)))
   27.38 -      | mk (Multiplied (n, j))  = (trace_msg ("*" ^ string_of_int n); trace_thm "*" (mult_thm (n, mk j)))
   27.39 +    fun mk (Asm i) = trace_thm ctxt ("Asm " ^ string_of_int i) (nth asms i)
   27.40 +      | mk (Nat i) = trace_thm ctxt ("Nat " ^ string_of_int i) (LA_Logic.mk_nat_thm thy (nth atoms i))
   27.41 +      | mk (LessD j) = trace_thm ctxt "L" (hd ([mk j] RL lessD))
   27.42 +      | mk (NotLeD j) = trace_thm ctxt "NLe" (mk j RS LA_Logic.not_leD)
   27.43 +      | mk (NotLeDD j) = trace_thm ctxt "NLeD" (hd ([mk j RS LA_Logic.not_leD] RL lessD))
   27.44 +      | mk (NotLessD j) = trace_thm ctxt "NL" (mk j RS LA_Logic.not_lessD)
   27.45 +      | mk (Added (j1, j2)) = simp (trace_thm ctxt "+" (add_thms (mk j1) (mk j2)))
   27.46 +      | mk (Multiplied (n, j)) =
   27.47 +          (trace_msg ("*" ^ string_of_int n); trace_thm ctxt "*" (mult_thm (n, mk j)))
   27.48  
   27.49    in
   27.50      let
   27.51        val _ = trace_msg "mkthm";
   27.52 -      val thm = trace_thm "Final thm:" (mk just);
   27.53 +      val thm = trace_thm ctxt "Final thm:" (mk just);
   27.54        val fls = simplify simpset' thm;
   27.55 -      val _ = trace_thm "After simplification:" fls;
   27.56 +      val _ = trace_thm ctxt "After simplification:" fls;
   27.57        val _ =
   27.58          if LA_Logic.is_False fls then ()
   27.59          else
   27.60 @@ -536,15 +537,15 @@
   27.61              if count > warning_count_max then ()
   27.62              else
   27.63                (tracing (cat_lines
   27.64 -                (["Assumptions:"] @ map Display.string_of_thm asms @ [""] @
   27.65 -                 ["Proved:", Display.string_of_thm fls, ""] @
   27.66 +                (["Assumptions:"] @ map (Display.string_of_thm ctxt) asms @ [""] @
   27.67 +                 ["Proved:", Display.string_of_thm ctxt fls, ""] @
   27.68                   (if count <> warning_count_max then []
   27.69                    else ["\n(Reached maximal message count -- disabling future warnings)"])));
   27.70                  warning "Linear arithmetic should have refuted the assumptions.\n\
   27.71                    \Please inform Tobias Nipkow (nipkow@in.tum.de).")
   27.72            end;
   27.73      in fls end
   27.74 -    handle FalseE thm => trace_thm "False reached early:" thm
   27.75 +    handle FalseE thm => trace_thm ctxt "False reached early:" thm
   27.76    end;
   27.77  
   27.78  end;
   27.79 @@ -775,8 +776,9 @@
   27.80    fn state =>
   27.81      let
   27.82        val ctxt = Simplifier.the_context ss;
   27.83 -      val _ = trace_thm ("refute_tac (on subgoal " ^ string_of_int i ^ ", with " ^
   27.84 -                             string_of_int (length justs) ^ " justification(s)):") state
   27.85 +      val _ = trace_thm ctxt
   27.86 +        ("refute_tac (on subgoal " ^ string_of_int i ^ ", with " ^
   27.87 +          string_of_int (length justs) ^ " justification(s)):") state
   27.88        val {neqE, ...} = get_data ctxt;
   27.89        fun just1 j =
   27.90          (* eliminate inequalities *)
   27.91 @@ -784,7 +786,7 @@
   27.92            REPEAT_DETERM (eresolve_tac neqE i)
   27.93          else
   27.94            all_tac) THEN
   27.95 -          PRIMITIVE (trace_thm "State after neqE:") THEN
   27.96 +          PRIMITIVE (trace_thm ctxt "State after neqE:") THEN
   27.97            (* use theorems generated from the actual justifications *)
   27.98            METAHYPS (fn asms => rtac (mkthm ss asms j) 1) i
   27.99      in
  27.100 @@ -792,7 +794,7 @@
  27.101        DETERM (resolve_tac [LA_Logic.notI, LA_Logic.ccontr] i) THEN
  27.102        (* user-defined preprocessing of the subgoal *)
  27.103        DETERM (LA_Data.pre_tac ctxt i) THEN
  27.104 -      PRIMITIVE (trace_thm "State after pre_tac:") THEN
  27.105 +      PRIMITIVE (trace_thm ctxt "State after pre_tac:") THEN
  27.106        (* prove every resulting subgoal, using its justification *)
  27.107        EVERY (map just1 justs)
  27.108      end  state;
  27.109 @@ -881,7 +883,7 @@
  27.110      val (Falsethm, _) = fwdproof ss tree js
  27.111      val contr = if pos then LA_Logic.ccontr else LA_Logic.notI
  27.112      val concl = implies_intr cnTconcl Falsethm COMP contr
  27.113 -  in SOME (trace_thm "Proved by lin. arith. prover:" (LA_Logic.mk_Eq concl)) end
  27.114 +  in SOME (trace_thm ctxt "Proved by lin. arith. prover:" (LA_Logic.mk_Eq concl)) end
  27.115    (*in case concl contains ?-var, which makes assume fail:*)   (* FIXME Variable.import_terms *)
  27.116    handle THM _ => NONE;
  27.117  
    28.1 --- a/src/Provers/blast.ML	Tue Jul 21 00:56:19 2009 +0200
    28.2 +++ b/src/Provers/blast.ML	Tue Jul 21 01:03:18 2009 +0200
    28.3 @@ -492,7 +492,9 @@
    28.4  end;
    28.5  
    28.6  
    28.7 -fun TRACE rl tac st i = if !trace then (Display.prth rl; tac st i) else tac st i;
    28.8 +fun TRACE rl tac st i =
    28.9 +  if !trace then (writeln (Display.string_of_thm_without_context rl); tac st i)
   28.10 +  else tac st i;
   28.11  
   28.12  (*Resolution/matching tactics: if upd then the proof state may be updated.
   28.13    Matching makes the tactics more deterministic in the presence of Vars.*)
   28.14 @@ -509,14 +511,16 @@
   28.15          THEN
   28.16          rot_subgoals_tac (rot, #2 trl) i
   28.17    in Option.SOME (trl, tac) end
   28.18 -  handle ElimBadPrem => (*reject: prems don't preserve conclusion*)
   28.19 -            (warning("Ignoring weak elimination rule\n" ^ Display.string_of_thm rl);
   28.20 -             Option.NONE)
   28.21 -       | ElimBadConcl => (*ignore: conclusion is not just a variable*)
   28.22 -           (if !trace then (warning("Ignoring ill-formed elimination rule:\n" ^
   28.23 -                       "conclusion should be a variable\n" ^ Display.string_of_thm rl))
   28.24 -            else ();
   28.25 -            Option.NONE);
   28.26 +  handle
   28.27 +    ElimBadPrem => (*reject: prems don't preserve conclusion*)
   28.28 +      (warning ("Ignoring weak elimination rule\n" ^ Display.string_of_thm_global thy rl);
   28.29 +        Option.NONE)
   28.30 +  | ElimBadConcl => (*ignore: conclusion is not just a variable*)
   28.31 +      (if !trace then
   28.32 +        (warning ("Ignoring ill-formed elimination rule:\n" ^
   28.33 +          "conclusion should be a variable\n" ^ Display.string_of_thm_global thy rl))
   28.34 +       else ();
   28.35 +       Option.NONE);
   28.36  
   28.37  
   28.38  (*** Conversion of Introduction Rules ***)
    29.1 --- a/src/Provers/classical.ML	Tue Jul 21 00:56:19 2009 +0200
    29.2 +++ b/src/Provers/classical.ML	Tue Jul 21 01:03:18 2009 +0200
    29.3 @@ -256,7 +256,7 @@
    29.4       xtra_netpair  = empty_netpair};
    29.5  
    29.6  fun print_cs (CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, ...}) =
    29.7 -  let val pretty_thms = map Display.pretty_thm in
    29.8 +  let val pretty_thms = map Display.pretty_thm_without_context in
    29.9      [Pretty.big_list "safe introduction rules (intro!):" (pretty_thms safeIs),
   29.10        Pretty.big_list "introduction rules (intro):" (pretty_thms hazIs),
   29.11        Pretty.big_list "safe elimination rules (elim!):" (pretty_thms safeEs),
   29.12 @@ -313,14 +313,18 @@
   29.13  (*Warn if the rule is already present ELSEWHERE in the claset.  The addition
   29.14    is still allowed.*)
   29.15  fun warn_dup th (CS{safeIs, safeEs, hazIs, hazEs, ...}) =
   29.16 -       if mem_thm safeIs th then
   29.17 -         warning ("Rule already declared as safe introduction (intro!)\n" ^ Display.string_of_thm th)
   29.18 +  if mem_thm safeIs th then
   29.19 +    warning ("Rule already declared as safe introduction (intro!)\n" ^
   29.20 +      Display.string_of_thm_without_context th)
   29.21    else if mem_thm safeEs th then
   29.22 -         warning ("Rule already declared as safe elimination (elim!)\n" ^ Display.string_of_thm th)
   29.23 +    warning ("Rule already declared as safe elimination (elim!)\n" ^
   29.24 +      Display.string_of_thm_without_context th)
   29.25    else if mem_thm hazIs th then
   29.26 -         warning ("Rule already declared as introduction (intro)\n" ^ Display.string_of_thm th)
   29.27 +    warning ("Rule already declared as introduction (intro)\n" ^
   29.28 +      Display.string_of_thm_without_context th)
   29.29    else if mem_thm hazEs th then
   29.30 -         warning ("Rule already declared as elimination (elim)\n" ^ Display.string_of_thm th)
   29.31 +    warning ("Rule already declared as elimination (elim)\n" ^
   29.32 +      Display.string_of_thm_without_context th)
   29.33    else ();
   29.34  
   29.35  
   29.36 @@ -330,8 +334,8 @@
   29.37    (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   29.38               safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   29.39    if mem_thm safeIs th then
   29.40 -         (warning ("Ignoring duplicate safe introduction (intro!)\n" ^ Display.string_of_thm th);
   29.41 -          cs)
   29.42 +    (warning ("Ignoring duplicate safe introduction (intro!)\n" ^
   29.43 +      Display.string_of_thm_without_context th); cs)
   29.44    else
   29.45    let val th' = flat_rule th
   29.46        val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*)
   29.47 @@ -356,10 +360,10 @@
   29.48    (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   29.49               safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   29.50    if mem_thm safeEs th then
   29.51 -         (warning ("Ignoring duplicate safe elimination (elim!)\n" ^ Display.string_of_thm th);
   29.52 -          cs)
   29.53 +    (warning ("Ignoring duplicate safe elimination (elim!)\n" ^
   29.54 +        Display.string_of_thm_without_context th); cs)
   29.55    else if has_fewer_prems 1 th then
   29.56 -    	error("Ill-formed elimination rule\n" ^ Display.string_of_thm th)
   29.57 +    	error ("Ill-formed elimination rule\n" ^ Display.string_of_thm_without_context th)
   29.58    else
   29.59    let
   29.60        val th' = classical_rule (flat_rule th)
   29.61 @@ -386,7 +390,7 @@
   29.62  
   29.63  fun make_elim th =
   29.64      if has_fewer_prems 1 th then
   29.65 -    	error("Ill-formed destruction rule\n" ^ Display.string_of_thm th)
   29.66 +    	  error ("Ill-formed destruction rule\n" ^ Display.string_of_thm_without_context th)
   29.67      else Tactic.make_elim th;
   29.68  
   29.69  fun cs addSDs ths = cs addSEs (map make_elim ths);
   29.70 @@ -398,8 +402,8 @@
   29.71    (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   29.72               safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   29.73    if mem_thm hazIs th then
   29.74 -         (warning ("Ignoring duplicate introduction (intro)\n" ^ Display.string_of_thm th);
   29.75 -          cs)
   29.76 +    (warning ("Ignoring duplicate introduction (intro)\n" ^
   29.77 +        Display.string_of_thm_without_context th); cs)
   29.78    else
   29.79    let val th' = flat_rule th
   29.80        val nI = length hazIs + 1
   29.81 @@ -418,16 +422,16 @@
   29.82          xtra_netpair = insert' (the_default 1 w) (nI,nE) ([th], []) xtra_netpair}
   29.83    end
   29.84    handle THM("RSN: no unifiers",_,_) => (*from dup_intr*)
   29.85 -         error ("Ill-formed introduction rule\n" ^ Display.string_of_thm th);
   29.86 +    error ("Ill-formed introduction rule\n" ^ Display.string_of_thm_without_context th);
   29.87  
   29.88  fun addE w th
   29.89    (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   29.90              safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   29.91    if mem_thm hazEs th then
   29.92 -         (warning ("Ignoring duplicate elimination (elim)\n" ^ Display.string_of_thm th);
   29.93 -          cs)
   29.94 +    (warning ("Ignoring duplicate elimination (elim)\n" ^
   29.95 +        Display.string_of_thm_without_context th); cs)
   29.96    else if has_fewer_prems 1 th then
   29.97 -    	error("Ill-formed elimination rule\n" ^ Display.string_of_thm th)
   29.98 +    	error("Ill-formed elimination rule\n" ^ Display.string_of_thm_without_context th)
   29.99    else
  29.100    let
  29.101        val th' = classical_rule (flat_rule th)
  29.102 @@ -519,7 +523,7 @@
  29.103      end
  29.104   else cs
  29.105   handle THM("RSN: no unifiers",_,_) => (*from dup_intr*)
  29.106 -        error ("Ill-formed introduction rule\n" ^ Display.string_of_thm th);
  29.107 +   error ("Ill-formed introduction rule\n" ^ Display.string_of_thm_without_context th);
  29.108  
  29.109  
  29.110  fun delE th
  29.111 @@ -548,7 +552,7 @@
  29.112        mem_thm hazIs th orelse mem_thm hazEs th orelse
  29.113        mem_thm safeEs th' orelse mem_thm hazEs th'
  29.114      then delSI th (delSE th (delI th (delE th (delSE th' (delE th' cs)))))
  29.115 -    else (warning ("Undeclared classical rule\n" ^ Display.string_of_thm th); cs)
  29.116 +    else (warning ("Undeclared classical rule\n" ^ Display.string_of_thm_without_context th); cs)
  29.117    end;
  29.118  
  29.119  fun cs delrules ths = fold delrule ths cs;
    30.1 --- a/src/Pure/Isar/args.ML	Tue Jul 21 00:56:19 2009 +0200
    30.2 +++ b/src/Pure/Isar/args.ML	Tue Jul 21 01:03:18 2009 +0200
    30.3 @@ -88,7 +88,7 @@
    30.4  
    30.5  fun pretty_src ctxt src =
    30.6    let
    30.7 -    val prt_thm = Pretty.backquote o ProofContext.pretty_thm ctxt;
    30.8 +    val prt_thm = Pretty.backquote o Display.pretty_thm ctxt;
    30.9      fun prt arg =
   30.10        (case T.get_value arg of
   30.11          SOME (T.Text s) => Pretty.str (quote s)
    31.1 --- a/src/Pure/Isar/calculation.ML	Tue Jul 21 00:56:19 2009 +0200
    31.2 +++ b/src/Pure/Isar/calculation.ML	Tue Jul 21 01:03:18 2009 +0200
    31.3 @@ -40,8 +40,8 @@
    31.4  fun print_rules ctxt =
    31.5    let val ((trans, sym), _) = CalculationData.get (Context.Proof ctxt) in
    31.6      [Pretty.big_list "transitivity rules:"
    31.7 -        (map (ProofContext.pretty_thm ctxt) (Item_Net.content trans)),
    31.8 -      Pretty.big_list "symmetry rules:" (map (ProofContext.pretty_thm ctxt) sym)]
    31.9 +        (map (Display.pretty_thm ctxt) (Item_Net.content trans)),
   31.10 +      Pretty.big_list "symmetry rules:" (map (Display.pretty_thm ctxt) sym)]
   31.11      |> Pretty.chunks |> Pretty.writeln
   31.12    end;
   31.13  
    32.1 --- a/src/Pure/Isar/code.ML	Tue Jul 21 00:56:19 2009 +0200
    32.2 +++ b/src/Pure/Isar/code.ML	Tue Jul 21 01:03:18 2009 +0200
    32.3 @@ -243,7 +243,7 @@
    32.4    (*default flag, theorems with proper flag (perhaps lazy)*)
    32.5  
    32.6  fun pretty_lthms ctxt r = case Lazy.peek r
    32.7 - of SOME thms => map (ProofContext.pretty_thm ctxt o fst) (Exn.release thms)
    32.8 + of SOME thms => map (Display.pretty_thm ctxt o fst) (Exn.release thms)
    32.9    | NONE => [Pretty.str "[...]"];
   32.10  
   32.11  fun certificate thy f r =
   32.12 @@ -263,7 +263,8 @@
   32.13        Pattern.matchess thy (args, (map incr_idx o curry Library.take (length args)) args');
   32.14      fun drop (thm', proper') = if (proper orelse not proper')
   32.15        andalso matches_args (args_of thm') then 
   32.16 -        (warning ("Code generator: dropping redundant code equation\n" ^ Display.string_of_thm thm'); true)
   32.17 +        (warning ("Code generator: dropping redundant code equation\n" ^
   32.18 +            Display.string_of_thm_global thy thm'); true)
   32.19        else false;
   32.20    in (thm, proper) :: filter_out drop thms end;
   32.21  
   32.22 @@ -567,16 +568,16 @@
   32.23  fun gen_assert_eqn thy is_constr_pat (thm, proper) =
   32.24    let
   32.25      val (lhs, rhs) = (Logic.dest_equals o Thm.plain_prop_of) thm
   32.26 -      handle TERM _ => bad_thm ("Not an equation: " ^ Display.string_of_thm thm)
   32.27 -           | THM _ => bad_thm ("Not an equation: " ^ Display.string_of_thm thm);
   32.28 +      handle TERM _ => bad_thm ("Not an equation: " ^ Display.string_of_thm_global thy thm)
   32.29 +           | THM _ => bad_thm ("Not an equation: " ^ Display.string_of_thm_global thy thm);
   32.30      fun vars_of t = fold_aterms (fn Var (v, _) => insert (op =) v
   32.31        | Free _ => bad_thm ("Illegal free variable in equation\n"
   32.32 -          ^ Display.string_of_thm thm)
   32.33 +          ^ Display.string_of_thm_global thy thm)
   32.34        | _ => I) t [];
   32.35      fun tvars_of t = fold_term_types (fn _ =>
   32.36        fold_atyps (fn TVar (v, _) => insert (op =) v
   32.37          | TFree _ => bad_thm 
   32.38 -      ("Illegal free type variable in equation\n" ^ Display.string_of_thm thm))) t [];
   32.39 +      ("Illegal free type variable in equation\n" ^ Display.string_of_thm_global thy thm))) t [];
   32.40      val lhs_vs = vars_of lhs;
   32.41      val rhs_vs = vars_of rhs;
   32.42      val lhs_tvs = tvars_of lhs;
   32.43 @@ -584,47 +585,48 @@
   32.44      val _ = if null (subtract (op =) lhs_vs rhs_vs)
   32.45        then ()
   32.46        else bad_thm ("Free variables on right hand side of equation\n"
   32.47 -        ^ Display.string_of_thm thm);
   32.48 +        ^ Display.string_of_thm_global thy thm);
   32.49      val _ = if null (subtract (op =) lhs_tvs rhs_tvs)
   32.50        then ()
   32.51        else bad_thm ("Free type variables on right hand side of equation\n"
   32.52 -        ^ Display.string_of_thm thm)    val (head, args) = (strip_comb o fst o Logic.dest_equals o Thm.plain_prop_of) thm;
   32.53 +        ^ Display.string_of_thm_global thy thm)
   32.54 +    val (head, args) = (strip_comb o fst o Logic.dest_equals o Thm.plain_prop_of) thm;
   32.55      val (c, ty) = case head
   32.56       of Const (c_ty as (_, ty)) => (AxClass.unoverload_const thy c_ty, ty)
   32.57 -      | _ => bad_thm ("Equation not headed by constant\n" ^ Display.string_of_thm thm);
   32.58 +      | _ => bad_thm ("Equation not headed by constant\n" ^ Display.string_of_thm_global thy thm);
   32.59      fun check _ (Abs _) = bad_thm
   32.60            ("Abstraction on left hand side of equation\n"
   32.61 -            ^ Display.string_of_thm thm)
   32.62 +            ^ Display.string_of_thm_global thy thm)
   32.63        | check 0 (Var _) = ()
   32.64        | check _ (Var _) = bad_thm
   32.65            ("Variable with application on left hand side of equation\n"
   32.66 -            ^ Display.string_of_thm thm)
   32.67 +            ^ Display.string_of_thm_global thy thm)
   32.68        | check n (t1 $ t2) = (check (n+1) t1; check 0 t2)
   32.69        | check n (Const (c_ty as (c, ty))) = if n = (length o fst o strip_type) ty
   32.70            then if not proper orelse is_constr_pat (AxClass.unoverload_const thy c_ty)
   32.71              then ()
   32.72              else bad_thm (quote c ^ " is not a constructor, on left hand side of equation\n"
   32.73 -              ^ Display.string_of_thm thm)
   32.74 +              ^ Display.string_of_thm_global thy thm)
   32.75            else bad_thm
   32.76              ("Partially applied constant " ^ quote c ^ " on left hand side of equation\n"
   32.77 -               ^ Display.string_of_thm thm);
   32.78 +               ^ Display.string_of_thm_global thy thm);
   32.79      val _ = map (check 0) args;
   32.80      val _ = if not proper orelse is_linear thm then ()
   32.81        else bad_thm ("Duplicate variables on left hand side of equation\n"
   32.82 -        ^ Display.string_of_thm thm);
   32.83 +        ^ Display.string_of_thm_global thy thm);
   32.84      val _ = if (is_none o AxClass.class_of_param thy) c
   32.85        then ()
   32.86        else bad_thm ("Polymorphic constant as head in equation\n"
   32.87 -        ^ Display.string_of_thm thm)
   32.88 +        ^ Display.string_of_thm_global thy thm)
   32.89      val _ = if not (is_constr thy c)
   32.90        then ()
   32.91        else bad_thm ("Constructor as head in equation\n"
   32.92 -        ^ Display.string_of_thm thm)
   32.93 +        ^ Display.string_of_thm_global thy thm)
   32.94      val ty_decl = Sign.the_const_type thy c;
   32.95      val _ = if Sign.typ_equiv thy (Type.strip_sorts ty_decl, Type.strip_sorts ty)
   32.96        then () else bad_thm ("Type\n" ^ string_of_typ thy ty
   32.97             ^ "\nof equation\n"
   32.98 -           ^ Display.string_of_thm thm
   32.99 +           ^ Display.string_of_thm_global thy thm
  32.100             ^ "\nis incompatible with declared function type\n"
  32.101             ^ string_of_typ thy ty_decl)
  32.102    in (thm, proper) end;
  32.103 @@ -657,7 +659,7 @@
  32.104    let
  32.105      fun cert (eqn as (thm, _)) = if c = const_eqn thy thm
  32.106        then eqn else error ("Wrong head of code equation,\nexpected constant "
  32.107 -        ^ string_of_const thy c ^ "\n" ^ Display.string_of_thm thm)
  32.108 +        ^ string_of_const thy c ^ "\n" ^ Display.string_of_thm_global thy thm)
  32.109    in map (cert o assert_eqn thy) eqns end;
  32.110  
  32.111  fun common_typ_eqns thy [] = []
  32.112 @@ -674,7 +676,7 @@
  32.113          fun unify ty env = Sign.typ_unify thy (ty1, ty) env
  32.114            handle Type.TUNIFY =>
  32.115              error ("Type unificaton failed, while unifying code equations\n"
  32.116 -            ^ (cat_lines o map Display.string_of_thm) thms
  32.117 +            ^ (cat_lines o map (Display.string_of_thm_global thy)) thms
  32.118              ^ "\nwith types\n"
  32.119              ^ (cat_lines o map (string_of_typ thy)) (ty1 :: tys));
  32.120          val (env, _) = fold unify tys (Vartab.empty, maxidx)
  32.121 @@ -796,15 +798,15 @@
  32.122    let
  32.123      val (ofclass, eqn) = case try Logic.dest_equals (Thm.prop_of thm)
  32.124       of SOME ofclass_eq => ofclass_eq
  32.125 -      | _ => error ("Bad certificate: " ^ Display.string_of_thm thm);
  32.126 +      | _ => error ("Bad certificate: " ^ Display.string_of_thm_global thy thm);
  32.127      val (T, class) = case try Logic.dest_of_class ofclass
  32.128       of SOME T_class => T_class
  32.129 -      | _ => error ("Bad certificate: " ^ Display.string_of_thm thm);
  32.130 +      | _ => error ("Bad certificate: " ^ Display.string_of_thm_global thy thm);
  32.131      val tvar = case try Term.dest_TVar T
  32.132       of SOME tvar => tvar
  32.133 -      | _ => error ("Bad type: " ^ Display.string_of_thm thm);
  32.134 +      | _ => error ("Bad type: " ^ Display.string_of_thm_global thy thm);
  32.135      val _ = if Term.add_tvars eqn [] = [tvar] then ()
  32.136 -      else error ("Inconsistent type: " ^ Display.string_of_thm thm);
  32.137 +      else error ("Inconsistent type: " ^ Display.string_of_thm_global thy thm);
  32.138      val lhs_rhs = case try Logic.dest_equals eqn
  32.139       of SOME lhs_rhs => lhs_rhs
  32.140        | _ => error ("Not an equation: " ^ Syntax.string_of_term_global thy eqn);
  32.141 @@ -813,7 +815,7 @@
  32.142        | _ => error ("Not an equation with two constants: "
  32.143            ^ Syntax.string_of_term_global thy eqn);
  32.144      val _ = if the_list (AxClass.class_of_param thy (snd c_c')) = [class] then ()
  32.145 -      else error ("Inconsistent class: " ^ Display.string_of_thm thm);
  32.146 +      else error ("Inconsistent class: " ^ Display.string_of_thm_global thy thm);
  32.147    in thy |>
  32.148      (map_exec_purge NONE o map_aliasses) (fn (alias, classes) =>
  32.149        ((c_c', thm) :: alias, insert (op =) class classes))
    33.1 --- a/src/Pure/Isar/context_rules.ML	Tue Jul 21 00:56:19 2009 +0200
    33.2 +++ b/src/Pure/Isar/context_rules.ML	Tue Jul 21 01:03:18 2009 +0200
    33.3 @@ -116,7 +116,7 @@
    33.4      fun prt_kind (i, b) =
    33.5        Pretty.big_list ((the o AList.lookup (op =) kind_names) (i, b) ^ ":")
    33.6          (map_filter (fn (_, (k, th)) =>
    33.7 -            if k = (i, b) then SOME (ProofContext.pretty_thm ctxt th) else NONE)
    33.8 +            if k = (i, b) then SOME (Display.pretty_thm ctxt th) else NONE)
    33.9            (sort (int_ord o pairself fst) rules));
   33.10    in Pretty.writeln (Pretty.chunks (map prt_kind rule_kinds)) end;
   33.11  
    34.1 --- a/src/Pure/Isar/element.ML	Tue Jul 21 00:56:19 2009 +0200
    34.2 +++ b/src/Pure/Isar/element.ML	Tue Jul 21 01:03:18 2009 +0200
    34.3 @@ -163,7 +163,7 @@
    34.4    let
    34.5      val prt_typ = Pretty.quote o Syntax.pretty_typ ctxt;
    34.6      val prt_term = Pretty.quote o Syntax.pretty_term ctxt;
    34.7 -    val prt_thm = Pretty.backquote o ProofContext.pretty_thm ctxt;
    34.8 +    val prt_thm = Pretty.backquote o Display.pretty_thm ctxt;
    34.9      val prt_name_atts = pretty_name_atts ctxt;
   34.10  
   34.11      fun prt_mixfix NoSyn = []
    35.1 --- a/src/Pure/Isar/isar_cmd.ML	Tue Jul 21 00:56:19 2009 +0200
    35.2 +++ b/src/Pure/Isar/isar_cmd.ML	Tue Jul 21 01:03:18 2009 +0200
    35.3 @@ -442,8 +442,7 @@
    35.4    |> Pretty.chunks2 |> Pretty.string_of;
    35.5  
    35.6  fun string_of_thms state args =
    35.7 -  Pretty.string_of (ProofContext.pretty_thms (Proof.context_of state)
    35.8 -    (Proof.get_thmss state args));
    35.9 +  Pretty.string_of (Display.pretty_thms (Proof.context_of state) (Proof.get_thmss state args));
   35.10  
   35.11  fun string_of_prfs full state arg =
   35.12    Pretty.string_of (case arg of
    36.1 --- a/src/Pure/Isar/local_defs.ML	Tue Jul 21 00:56:19 2009 +0200
    36.2 +++ b/src/Pure/Isar/local_defs.ML	Tue Jul 21 01:03:18 2009 +0200
    36.3 @@ -196,7 +196,7 @@
    36.4  
    36.5  fun print_rules ctxt =
    36.6    Pretty.writeln (Pretty.big_list "definitional transformations:"
    36.7 -    (map (ProofContext.pretty_thm ctxt) (Rules.get (Context.Proof ctxt))));
    36.8 +    (map (Display.pretty_thm ctxt) (Rules.get (Context.Proof ctxt))));
    36.9  
   36.10  val defn_add = Thm.declaration_attribute (Rules.map o Thm.add_thm);
   36.11  val defn_del = Thm.declaration_attribute (Rules.map o Thm.del_thm);
    37.1 --- a/src/Pure/Isar/method.ML	Tue Jul 21 00:56:19 2009 +0200
    37.2 +++ b/src/Pure/Isar/method.ML	Tue Jul 21 01:03:18 2009 +0200
    37.3 @@ -220,7 +220,7 @@
    37.4  
    37.5  fun trace ctxt rules =
    37.6    if ! trace_rules andalso not (null rules) then
    37.7 -    Pretty.big_list "rules:" (map (ProofContext.pretty_thm ctxt) rules)
    37.8 +    Pretty.big_list "rules:" (map (Display.pretty_thm ctxt) rules)
    37.9      |> Pretty.string_of |> tracing
   37.10    else ();
   37.11  
    38.1 --- a/src/Pure/Isar/obtain.ML	Tue Jul 21 00:56:19 2009 +0200
    38.2 +++ b/src/Pure/Isar/obtain.ML	Tue Jul 21 01:03:18 2009 +0200
    38.3 @@ -180,9 +180,9 @@
    38.4      [prem] =>
    38.5        if Thm.concl_of th aconv thesis andalso
    38.6          Logic.strip_assums_concl prem aconv thesis then th
    38.7 -      else error ("Guessed a different clause:\n" ^ ProofContext.string_of_thm ctxt th)
    38.8 +      else error ("Guessed a different clause:\n" ^ Display.string_of_thm ctxt th)
    38.9    | [] => error "Goal solved -- nothing guessed."
   38.10 -  | _ => error ("Guess split into several cases:\n" ^ ProofContext.string_of_thm ctxt th));
   38.11 +  | _ => error ("Guess split into several cases:\n" ^ Display.string_of_thm ctxt th));
   38.12  
   38.13  fun result tac facts ctxt =
   38.14    let
   38.15 @@ -218,7 +218,7 @@
   38.16      val string_of_typ = Syntax.string_of_typ ctxt;
   38.17      val string_of_term = setmp show_types true (Syntax.string_of_term ctxt);
   38.18  
   38.19 -    fun err msg th = error (msg ^ ":\n" ^ ProofContext.string_of_thm ctxt th);
   38.20 +    fun err msg th = error (msg ^ ":\n" ^ Display.string_of_thm ctxt th);
   38.21  
   38.22      val maxidx = fold (Term.maxidx_typ o snd o fst) vars ~1;
   38.23      val rule = Thm.incr_indexes (maxidx + 1) raw_rule;
    39.1 --- a/src/Pure/Isar/proof.ML	Tue Jul 21 00:56:19 2009 +0200
    39.2 +++ b/src/Pure/Isar/proof.ML	Tue Jul 21 01:03:18 2009 +0200
    39.3 @@ -322,7 +322,7 @@
    39.4  
    39.5  fun pretty_facts _ _ NONE = []
    39.6    | pretty_facts s ctxt (SOME ths) =
    39.7 -      [Pretty.big_list (s ^ "this:") (map (ProofContext.pretty_thm ctxt) ths), Pretty.str ""];
    39.8 +      [Pretty.big_list (s ^ "this:") (map (Display.pretty_thm ctxt) ths), Pretty.str ""];
    39.9  
   39.10  fun pretty_state nr state =
   39.11    let
   39.12 @@ -470,7 +470,7 @@
   39.13    let
   39.14      val thy = ProofContext.theory_of ctxt;
   39.15      val string_of_term = Syntax.string_of_term ctxt;
   39.16 -    val string_of_thm = ProofContext.string_of_thm ctxt;
   39.17 +    val string_of_thm = Display.string_of_thm ctxt;
   39.18  
   39.19      val ngoals = Thm.nprems_of goal;
   39.20      val _ = ngoals = 0 orelse error (Pretty.string_of (Pretty.chunks
    40.1 --- a/src/Pure/Isar/proof_display.ML	Tue Jul 21 00:56:19 2009 +0200
    40.2 +++ b/src/Pure/Isar/proof_display.ML	Tue Jul 21 01:03:18 2009 +0200
    40.3 @@ -35,7 +35,7 @@
    40.4    let
    40.5      val thy = Thm.theory_of_thm th;
    40.6      val flags = {quote = true, show_hyps = false, show_status = true};
    40.7 -  in Display.pretty_thm_aux (Syntax.pp_global thy) flags [] th end;
    40.8 +  in Display.pretty_thm_raw (Syntax.pp_global thy) flags [] th end;
    40.9  
   40.10  val pp_typ = Pretty.quote oo Syntax.pretty_typ_global;
   40.11  val pp_term = Pretty.quote oo Syntax.pretty_term_global;
   40.12 @@ -68,7 +68,7 @@
   40.13  
   40.14  fun pretty_rule ctxt s thm =
   40.15    Pretty.block [Pretty.str (s ^ " attempt to solve goal by exported rule:"),
   40.16 -    Pretty.fbrk, ProofContext.pretty_thm_aux ctxt false thm];
   40.17 +    Pretty.fbrk, Display.pretty_thm_aux ctxt false thm];
   40.18  
   40.19  val string_of_rule = Pretty.string_of ooo pretty_rule;
   40.20  
    41.1 --- a/src/Pure/Isar/runtime.ML	Tue Jul 21 00:56:19 2009 +0200
    41.2 +++ b/src/Pure/Isar/runtime.ML	Tue Jul 21 01:03:18 2009 +0200
    41.3 @@ -75,7 +75,7 @@
    41.4        | exn_msg ctxt (exn as TERM (msg, ts)) = raised exn "TERM" (msg ::
    41.5              (if detailed then if_context ctxt Syntax.string_of_term ts else []))
    41.6        | exn_msg ctxt (exn as THM (msg, i, thms)) = raised exn ("THM " ^ string_of_int i) (msg ::
    41.7 -            (if detailed then if_context ctxt ProofContext.string_of_thm thms else []))
    41.8 +            (if detailed then if_context ctxt Display.string_of_thm thms else []))
    41.9        | exn_msg _ exn = raised exn (General.exnMessage exn) [];
   41.10    in exn_msg NONE e end;
   41.11  
    42.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Tue Jul 21 00:56:19 2009 +0200
    42.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Tue Jul 21 01:03:18 2009 +0200
    42.3 @@ -655,7 +655,7 @@
    42.4                                    text=[XML.Elem("pgml",[],
    42.5                                                   maps YXML.parse_body strings)] })
    42.6  
    42.7 -        fun string_of_thm th = Pretty.string_of (Display.pretty_thm_aux
    42.8 +        fun string_of_thm th = Pretty.string_of (Display.pretty_thm_raw
    42.9              (Syntax.pp_global (Thm.theory_of_thm th))
   42.10              {quote = false, show_hyps = false, show_status = true} [] th)
   42.11  
    43.1 --- a/src/Pure/Tools/find_theorems.ML	Tue Jul 21 00:56:19 2009 +0200
    43.2 +++ b/src/Pure/Tools/find_theorems.ML	Tue Jul 21 01:03:18 2009 +0200
    43.3 @@ -408,7 +408,7 @@
    43.4  
    43.5  fun pretty_thm ctxt (thmref, thm) = Pretty.block
    43.6    [Pretty.str (Facts.string_of_ref thmref), Pretty.str ":", Pretty.brk 1,
    43.7 -    ProofContext.pretty_thm ctxt thm];
    43.8 +    Display.pretty_thm ctxt thm];
    43.9  
   43.10  fun print_theorems ctxt opt_goal opt_limit rem_dups raw_criteria =
   43.11    let
    44.1 --- a/src/Pure/old_goals.ML	Tue Jul 21 00:56:19 2009 +0200
    44.2 +++ b/src/Pure/old_goals.ML	Tue Jul 21 01:03:18 2009 +0200
    44.3 @@ -199,7 +199,7 @@
    44.4    case e of
    44.5       THM (msg,i,thms) =>
    44.6           (writeln ("Exception THM " ^ string_of_int i ^ " raised:\n" ^ msg);
    44.7 -          List.app Display.print_thm thms)
    44.8 +          List.app (writeln o Display.string_of_thm_global thy) thms)
    44.9     | THEORY (msg,thys) =>
   44.10           (writeln ("Exception THEORY raised:\n" ^ msg);
   44.11            List.app (writeln o Context.str_of_thy) thys)
    45.1 --- a/src/Pure/simplifier.ML	Tue Jul 21 00:56:19 2009 +0200
    45.2 +++ b/src/Pure/simplifier.ML	Tue Jul 21 01:03:18 2009 +0200
    45.3 @@ -79,7 +79,7 @@
    45.4  fun pretty_ss ctxt ss =
    45.5    let
    45.6      val pretty_cterm = Syntax.pretty_term ctxt o Thm.term_of;
    45.7 -    val pretty_thm = ProofContext.pretty_thm ctxt;
    45.8 +    val pretty_thm = Display.pretty_thm ctxt;
    45.9      fun pretty_proc (name, lhss) = Pretty.big_list (name ^ ":") (map pretty_cterm lhss);
   45.10      fun pretty_cong (name, thm) =
   45.11        Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 1, pretty_thm thm];
    46.1 --- a/src/Sequents/prover.ML	Tue Jul 21 00:56:19 2009 +0200
    46.2 +++ b/src/Sequents/prover.ML	Tue Jul 21 01:03:18 2009 +0200
    46.3 @@ -27,7 +27,8 @@
    46.4  
    46.5  fun warn_duplicates [] = []
    46.6    | warn_duplicates dups =
    46.7 -      (warning (cat_lines ("Ignoring duplicate theorems:" :: map Display.string_of_thm dups));
    46.8 +      (warning (cat_lines ("Ignoring duplicate theorems:" ::
    46.9 +          map Display.string_of_thm_without_context dups));
   46.10         dups);
   46.11  
   46.12  fun (Pack(safes,unsafes)) add_safes ths   = 
   46.13 @@ -50,8 +51,9 @@
   46.14  
   46.15  
   46.16  fun print_pack (Pack(safes,unsafes)) =
   46.17 -    (writeln "Safe rules:";  Display.print_thms safes;
   46.18 -     writeln "Unsafe rules:"; Display.print_thms unsafes);
   46.19 +  writeln (cat_lines
   46.20 +   (["Safe rules:"] @ map Display.string_of_thm_without_context safes @
   46.21 +    ["Unsafe rules:"] @ map Display.string_of_thm_without_context unsafes));
   46.22  
   46.23  (*Returns the list of all formulas in the sequent*)
   46.24  fun forms_of_seq (Const("SeqO'",_) $ P $ u) = P :: forms_of_seq u
    47.1 --- a/src/Sequents/simpdata.ML	Tue Jul 21 00:56:19 2009 +0200
    47.2 +++ b/src/Sequents/simpdata.ML	Tue Jul 21 01:03:18 2009 +0200
    47.3 @@ -40,7 +40,7 @@
    47.4                      | (Const("Not",_)$_)      => th RS @{thm iff_reflection_F}
    47.5                      | _                       => th RS @{thm iff_reflection_T})
    47.6             | _ => error ("addsimps: unable to use theorem\n" ^
    47.7 -                         Display.string_of_thm th));
    47.8 +                         Display.string_of_thm_without_context th));
    47.9  
   47.10  (*Replace premises x=y, X<->Y by X==Y*)
   47.11  val mk_meta_prems =
    48.1 --- a/src/Tools/Code/code_preproc.ML	Tue Jul 21 00:56:19 2009 +0200
    48.2 +++ b/src/Tools/Code/code_preproc.ML	Tue Jul 21 01:03:18 2009 +0200
    48.3 @@ -210,7 +210,7 @@
    48.4    |> map (fn (s, thms) =>
    48.5         (Pretty.block o Pretty.fbreaks) (
    48.6           Pretty.str s
    48.7 -         :: map (Display.pretty_thm o fst) thms
    48.8 +         :: map (Display.pretty_thm_global thy o fst) thms
    48.9         ))
   48.10    |> Pretty.chunks;
   48.11  
   48.12 @@ -523,7 +523,7 @@
   48.13        in
   48.14          Thm.transitive thm1 (Thm.transitive thm2 thm3) handle THM _ =>
   48.15            error ("could not construct evaluation proof:\n"
   48.16 -          ^ (cat_lines o map Display.string_of_thm) [thm1, thm2, thm3])
   48.17 +          ^ (cat_lines o map (Display.string_of_thm_global thy)) [thm1, thm2, thm3])
   48.18        end;
   48.19    in gen_eval thy I conclude_evaluation end;
   48.20  
    49.1 --- a/src/Tools/Code/code_printer.ML	Tue Jul 21 00:56:19 2009 +0200
    49.2 +++ b/src/Tools/Code/code_printer.ML	Tue Jul 21 01:03:18 2009 +0200
    49.3 @@ -82,7 +82,7 @@
    49.4  
    49.5  open Code_Thingol;
    49.6  
    49.7 -fun nerror thm s = error (s ^ ",\nin equation " ^ Display.string_of_thm thm);
    49.8 +fun nerror thm s = error (s ^ ",\nin equation " ^ Display.string_of_thm_without_context thm);
    49.9  
   49.10  (** assembling text pieces **)
   49.11  
    50.1 --- a/src/Tools/Code/code_thingol.ML	Tue Jul 21 00:56:19 2009 +0200
    50.2 +++ b/src/Tools/Code/code_thingol.ML	Tue Jul 21 01:03:18 2009 +0200
    50.3 @@ -469,7 +469,7 @@
    50.4    let
    50.5      val err_class = Sorts.class_error (Syntax.pp_global thy) e;
    50.6      val err_thm = case thm
    50.7 -     of SOME thm => "\n(in code equation " ^ Display.string_of_thm thm ^ ")" | NONE => "";
    50.8 +     of SOME thm => "\n(in code equation " ^ Display.string_of_thm_global thy thm ^ ")" | NONE => "";
    50.9      val err_typ = "Type " ^ Syntax.string_of_typ_global thy ty ^ " not of sort "
   50.10        ^ Syntax.string_of_sort_global thy sort;
   50.11    in error ("Wellsortedness error" ^ err_thm ^ ":\n" ^ err_typ ^ "\n" ^ err_class) end;
    51.1 --- a/src/Tools/coherent.ML	Tue Jul 21 00:56:19 2009 +0200
    51.2 +++ b/src/Tools/coherent.ML	Tue Jul 21 01:03:18 2009 +0200
    51.3 @@ -177,7 +177,7 @@
    51.4  fun thm_of_cl_prf thy goal asms (ClPrf (th, (tye, env), insts, is, prfs)) =
    51.5    let
    51.6      val _ = message (fn () => space_implode "\n"
    51.7 -      ("asms:" :: map Display.string_of_thm asms) ^ "\n\n");
    51.8 +      ("asms:" :: map (Display.string_of_thm_global thy) asms) ^ "\n\n");
    51.9      val th' = Drule.implies_elim_list
   51.10        (Thm.instantiate
   51.11           (map (fn (ixn, (S, T)) =>
    52.1 --- a/src/Tools/induct.ML	Tue Jul 21 00:56:19 2009 +0200
    52.2 +++ b/src/Tools/induct.ML	Tue Jul 21 01:03:18 2009 +0200
    52.3 @@ -124,7 +124,7 @@
    52.4  
    52.5  fun pretty_rules ctxt kind rs =
    52.6    let val thms = map snd (Item_Net.content rs)
    52.7 -  in Pretty.big_list kind (map (ProofContext.pretty_thm ctxt) thms) end;
    52.8 +  in Pretty.big_list kind (map (Display.pretty_thm ctxt) thms) end;
    52.9  
   52.10  
   52.11  (* context data *)
    53.1 --- a/src/ZF/Tools/inductive_package.ML	Tue Jul 21 00:56:19 2009 +0200
    53.2 +++ b/src/ZF/Tools/inductive_package.ML	Tue Jul 21 01:03:18 2009 +0200
    53.3 @@ -247,8 +247,7 @@
    53.4      (intr_tms, map intro_tacsf (mk_disj_rls (length intr_tms)))
    53.5      |> ListPair.map (fn (t, tacs) =>
    53.6        Goal.prove_global thy1 [] [] t
    53.7 -        (fn _ => EVERY (rewrite_goals_tac part_rec_defs :: tacs)))
    53.8 -    handle MetaSimplifier.SIMPLIFIER (msg, thm) => (Display.print_thm thm; error msg);
    53.9 +        (fn _ => EVERY (rewrite_goals_tac part_rec_defs :: tacs)));
   53.10  
   53.11    (********)
   53.12    val dummy = writeln "  Proving the elimination rule...";
   53.13 @@ -318,11 +317,12 @@
   53.14       val ind_prems = map (induct_prem (map (rpair pred) rec_tms))
   53.15                           intr_tms;
   53.16  
   53.17 -     val dummy = if !Ind_Syntax.trace then
   53.18 -                 (writeln "ind_prems = ";
   53.19 -                  List.app (writeln o Syntax.string_of_term ctxt1) ind_prems;
   53.20 -                  writeln "raw_induct = "; Display.print_thm raw_induct)
   53.21 -             else ();
   53.22 +     val dummy =
   53.23 +      if ! Ind_Syntax.trace then
   53.24 +        writeln (cat_lines
   53.25 +          (["ind_prems:"] @ map (Syntax.string_of_term ctxt1) ind_prems @
   53.26 +           ["raw_induct:", Display.string_of_thm ctxt1 raw_induct]))
   53.27 +      else ();
   53.28  
   53.29  
   53.30       (*We use a MINIMAL simpset. Even FOL_ss contains too many simpules.
   53.31 @@ -351,9 +351,10 @@
   53.32                                 ORELSE' bound_hyp_subst_tac)),
   53.33              ind_tac (rev (map (rewrite_rule part_rec_defs) prems)) (length prems)]);
   53.34  
   53.35 -     val dummy = if !Ind_Syntax.trace then
   53.36 -                 (writeln "quant_induct = "; Display.print_thm quant_induct)
   53.37 -             else ();
   53.38 +     val dummy =
   53.39 +      if ! Ind_Syntax.trace then
   53.40 +        writeln ("quant_induct:\n" ^ Display.string_of_thm ctxt1 quant_induct)
   53.41 +      else ();
   53.42  
   53.43  
   53.44       (*** Prove the simultaneous induction rule ***)
   53.45 @@ -426,9 +427,10 @@
   53.46                  REPEAT (rewrite_goals_tac [Pr.split_eq] THEN lemma_tac 1)]))
   53.47         else (writeln "  [ No mutual induction rule needed ]"; @{thm TrueI});
   53.48  
   53.49 -     val dummy = if !Ind_Syntax.trace then
   53.50 -                 (writeln "lemma = "; Display.print_thm lemma)
   53.51 -             else ();
   53.52 +     val dummy =
   53.53 +      if ! Ind_Syntax.trace then
   53.54 +        writeln ("lemma: " ^ Display.string_of_thm ctxt1 lemma)
   53.55 +      else ();
   53.56  
   53.57  
   53.58       (*Mutual induction follows by freeness of Inl/Inr.*)
    54.1 --- a/src/ZF/Tools/typechk.ML	Tue Jul 21 00:56:19 2009 +0200
    54.2 +++ b/src/ZF/Tools/typechk.ML	Tue Jul 21 01:03:18 2009 +0200
    54.3 @@ -27,7 +27,8 @@
    54.4  
    54.5  fun add_rule th (tcs as TC {rules, net}) =
    54.6    if member Thm.eq_thm_prop rules th then
    54.7 -    (warning ("Ignoring duplicate type-checking rule\n" ^ Display.string_of_thm th); tcs)
    54.8 +    (warning ("Ignoring duplicate type-checking rule\n" ^
    54.9 +        Display.string_of_thm_without_context th); tcs)
   54.10    else
   54.11      TC {rules = th :: rules,
   54.12          net = Net.insert_term (K false) (Thm.concl_of th, th) net};
   54.13 @@ -36,7 +37,8 @@
   54.14    if member Thm.eq_thm_prop rules th then
   54.15      TC {net = Net.delete_term Thm.eq_thm_prop (Thm.concl_of th, th) net,
   54.16          rules = remove Thm.eq_thm_prop th rules}
   54.17 -  else (warning ("No such type-checking rule\n" ^ Display.string_of_thm th); tcs);
   54.18 +  else (warning ("No such type-checking rule\n" ^
   54.19 +    Display.string_of_thm_without_context th); tcs);
   54.20  
   54.21  
   54.22  (* generic data *)
   54.23 @@ -60,7 +62,7 @@
   54.24  fun print_tcset ctxt =
   54.25    let val TC {rules, ...} = tcset_of ctxt in
   54.26      Pretty.writeln (Pretty.big_list "type-checking rules:"
   54.27 -      (map (ProofContext.pretty_thm ctxt) rules))
   54.28 +      (map (Display.pretty_thm ctxt) rules))
   54.29    end;
   54.30  
   54.31