proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
--- a/src/FOLP/classical.ML Tue Jul 21 00:56:19 2009 +0200
+++ b/src/FOLP/classical.ML Tue Jul 21 01:03:18 2009 +0200
@@ -124,11 +124,11 @@
val empty_cs = make_cs{safeIs=[], safeEs=[], hazIs=[], hazEs=[]};
fun print_cs (CS{safeIs,safeEs,hazIs,hazEs,...}) =
- (writeln"Introduction rules"; Display.prths hazIs;
- writeln"Safe introduction rules"; Display.prths safeIs;
- writeln"Elimination rules"; Display.prths hazEs;
- writeln"Safe elimination rules"; Display.prths safeEs;
- ());
+ writeln (cat_lines
+ (["Introduction rules"] @ map Display.string_of_thm_without_context hazIs @
+ ["Safe introduction rules"] @ map Display.string_of_thm_without_context safeIs @
+ ["Elimination rules"] @ map Display.string_of_thm_without_context hazEs @
+ ["Safe elimination rules"] @ map Display.string_of_thm_without_context safeEs));
fun (CS{safeIs,safeEs,hazIs,hazEs,...}) addSIs ths =
make_cs {safeIs=ths@safeIs, safeEs=safeEs, hazIs=hazIs, hazEs=hazEs};
--- a/src/FOLP/ex/Prolog.ML Tue Jul 21 00:56:19 2009 +0200
+++ b/src/FOLP/ex/Prolog.ML Tue Jul 21 01:03:18 2009 +0200
@@ -13,7 +13,7 @@
by (resolve_tac [appNil,appCons] 1);
by (resolve_tac [appNil,appCons] 1);
by (resolve_tac [appNil,appCons] 1);
-prth (result());
+result();
Goal "app(?x, c:d:Nil, a:b:c:d:Nil)";
by (REPEAT (resolve_tac [appNil,appCons] 1));
--- a/src/FOLP/simp.ML Tue Jul 21 00:56:19 2009 +0200
+++ b/src/FOLP/simp.ML Tue Jul 21 01:03:18 2009 +0200
@@ -113,7 +113,7 @@
let fun norm thm =
case lhs_of(concl_of thm) of
Const(n,_)$_ => n
- | _ => (Display.prths normE_thms; error"No constant in lhs of a norm_thm")
+ | _ => error "No constant in lhs of a norm_thm"
in map norm normE_thms end;
fun lhs_is_NORM(thm,i) = case lhs_of_eq i thm of
@@ -122,7 +122,7 @@
val refl_tac = resolve_tac refl_thms;
fun find_res thms thm =
- let fun find [] = (Display.prths thms; error"Check Simp_Data")
+ let fun find [] = error "Check Simp_Data"
| find(th::thms) = thm RS th handle THM _ => find thms
in find thms end;
@@ -249,8 +249,8 @@
fun insert_thm_warn th net =
Net.insert_term Thm.eq_thm_prop (concl_of th, th) net
handle Net.INSERT =>
- (writeln"\nDuplicate rewrite or congruence rule:"; Display.print_thm th;
- net);
+ (writeln ("Duplicate rewrite or congruence rule:\n" ^
+ Display.string_of_thm_without_context th); net);
val insert_thms = fold_rev insert_thm_warn;
@@ -275,8 +275,8 @@
fun delete_thm_warn th net =
Net.delete_term Thm.eq_thm_prop (concl_of th, th) net
handle Net.DELETE =>
- (writeln"\nNo such rewrite or congruence rule:"; Display.print_thm th;
- net);
+ (writeln ("No such rewrite or congruence rule:\n" ^
+ Display.string_of_thm_without_context th); net);
val delete_thms = fold_rev delete_thm_warn;
@@ -290,9 +290,9 @@
fun delrew(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}, thm) =
let fun find((p as (th,ths))::ps',ps) =
if Thm.eq_thm_prop(thm,th) then (ths,ps@ps') else find(ps',p::ps)
- | find([],simps') = (writeln"\nNo such rewrite or congruence rule:";
- Display.print_thm thm;
- ([],simps'))
+ | find([],simps') =
+ (writeln ("No such rewrite or congruence rule:\n" ^
+ Display.string_of_thm_without_context thm); ([], simps'))
val (thms,simps') = find(simps,[])
in SS{auto_tac=auto_tac, congs=congs, cong_net=cong_net, mk_simps=mk_simps,
simps = simps', simp_net = delete_thms thms simp_net }
@@ -311,8 +311,9 @@
fun dest_ss(SS{congs,simps,...}) = (congs, map #1 simps);
fun print_ss(SS{congs,simps,...}) =
- (writeln"Congruences:"; Display.prths congs;
- writeln"Rewrite Rules:"; Display.prths (map #1 simps); ());
+ writeln (cat_lines
+ (["Congruences:"] @ map Display.string_of_thm_without_context congs @
+ ["Rewrite Rules:"] @ map (Display.string_of_thm_without_context o #1) simps));
(* Rewriting with conditionals *)
@@ -435,7 +436,8 @@
val rwrls = map mk_trans (List.concat(map mk_rew_rules thms));
val anet' = List.foldr lhs_insert_thm anet rwrls
in if !tracing andalso not(null new_rws)
- then (writeln"Adding rewrites:"; Display.prths new_rws; ())
+ then writeln (cat_lines
+ ("Adding rewrites:" :: map Display.string_of_thm_without_context new_rws))
else ();
(ss,thm,anet',anet::ats,cs)
end;
--- a/src/HOL/Import/import.ML Tue Jul 21 00:56:19 2009 +0200
+++ b/src/HOL/Import/import.ML Tue Jul 21 01:03:18 2009 +0200
@@ -44,9 +44,9 @@
val thm = equal_elim rew thm
val prew = ProofKernel.rewrite_hol4_term prem thy
val prem' = #2 (Logic.dest_equals (prop_of prew))
- val _ = message ("Import proved " ^ Display.string_of_thm thm)
+ val _ = message ("Import proved " ^ Display.string_of_thm ctxt thm)
val thm = ProofKernel.disambiguate_frees thm
- val _ = message ("Disambiguate: " ^ Display.string_of_thm thm)
+ val _ = message ("Disambiguate: " ^ Display.string_of_thm ctxt thm)
in
case Shuffler.set_prop thy prem' [("",thm)] of
SOME (_,thm) =>
--- a/src/HOL/Import/proof_kernel.ML Tue Jul 21 00:56:19 2009 +0200
+++ b/src/HOL/Import/proof_kernel.ML Tue Jul 21 01:03:18 2009 +0200
@@ -243,7 +243,7 @@
val smart_string_of_thm = smart_string_of_cterm o cprop_of
-fun prth th = writeln (PrintMode.setmp [] Display.string_of_thm th)
+fun prth th = writeln (PrintMode.setmp [] Display.string_of_thm_without_context th)
fun prc ct = writeln (PrintMode.setmp [] Display.string_of_cterm ct)
fun prin t = writeln (PrintMode.setmp [] (fn () => Syntax.string_of_term_global (the_context ()) t) ());
fun pth (HOLThm(ren,thm)) =
--- a/src/HOL/Import/shuffler.ML Tue Jul 21 00:56:19 2009 +0200
+++ b/src/HOL/Import/shuffler.ML Tue Jul 21 01:03:18 2009 +0200
@@ -40,7 +40,7 @@
case e of
THM (msg,i,thms) =>
(writeln ("Exception THM " ^ string_of_int i ^ " raised:\n" ^ msg);
- List.app Display.print_thm thms)
+ List.app (writeln o Display.string_of_thm_global sign) thms)
| THEORY (msg,thys) =>
(writeln ("Exception THEORY raised:\n" ^ msg);
List.app (writeln o Context.str_of_thy) thys)
@@ -56,7 +56,7 @@
(*Prints an exception, then fails*)
fun print_sign_exn sign e = (print_sign_exn_unit sign e; raise e)
-val string_of_thm = PrintMode.setmp [] Display.string_of_thm;
+val string_of_thm = PrintMode.setmp [] Display.string_of_thm_without_context;
val string_of_cterm = PrintMode.setmp [] Display.string_of_cterm;
fun mk_meta_eq th =
@@ -84,7 +84,7 @@
fun print_shuffles thy =
Pretty.writeln (Pretty.big_list "Shuffle theorems:"
- (map Display.pretty_thm (ShuffleData.get thy)))
+ (map (Display.pretty_thm_global thy) (ShuffleData.get thy)))
val weaken =
let
--- a/src/HOL/Nominal/nominal_thmdecls.ML Tue Jul 21 00:56:19 2009 +0200
+++ b/src/HOL/Nominal/nominal_thmdecls.ML Tue Jul 21 01:03:18 2009 +0200
@@ -156,7 +156,7 @@
fold (fn thm => Data.map (flag thm)) thms_to_be_added context
end
handle EQVT_FORM s =>
- error (Display.string_of_thm orig_thm ^
+ error (Display.string_of_thm (Context.proof_of context) orig_thm ^
" does not comply with the form of an equivariance lemma (" ^ s ^").")
--- a/src/HOL/Tools/TFL/casesplit.ML Tue Jul 21 00:56:19 2009 +0200
+++ b/src/HOL/Tools/TFL/casesplit.ML Tue Jul 21 01:03:18 2009 +0200
@@ -269,9 +269,9 @@
fun split th =
(case find_thms_split splitths 1 th of
NONE =>
- (writeln "th:";
- Display.print_thm th; writeln "split ths:";
- Display.print_thms splitths; writeln "\n--";
+ (writeln (cat_lines
+ (["th:", Display.string_of_thm_without_context th, "split ths:"] @
+ map Display.string_of_thm_without_context splitths @ ["\n--"]));
error "splitto: cannot find variable to split on")
| SOME v =>
let
--- a/src/HOL/Tools/TFL/rules.ML Tue Jul 21 00:56:19 2009 +0200
+++ b/src/HOL/Tools/TFL/rules.ML Tue Jul 21 01:03:18 2009 +0200
@@ -552,7 +552,7 @@
fun say s = if !tracing then writeln s else ();
fun print_thms s L =
- say (cat_lines (s :: map Display.string_of_thm L));
+ say (cat_lines (s :: map Display.string_of_thm_without_context L));
fun print_cterms s L =
say (cat_lines (s :: map Display.string_of_cterm L));
@@ -677,7 +677,7 @@
val cntxt = Simplifier.prems_of_ss ss
val dummy = print_thms "cntxt:" cntxt
val dummy = say "cong rule:"
- val dummy = say (Display.string_of_thm thm)
+ val dummy = say (Display.string_of_thm_without_context thm)
val dummy = thm_ref := (thm :: !thm_ref)
val dummy = ss_ref := (ss :: !ss_ref)
(* Unquantified eliminate *)
--- a/src/HOL/Tools/TFL/tfl.ML Tue Jul 21 00:56:19 2009 +0200
+++ b/src/HOL/Tools/TFL/tfl.ML Tue Jul 21 01:03:18 2009 +0200
@@ -529,9 +529,8 @@
val f = #lhs(S.dest_eq proto_def)
val (extractants,TCl) = ListPair.unzip extracta
val dummy = if !trace
- then (writeln "Extractants = ";
- Display.prths extractants;
- ())
+ then writeln (cat_lines ("Extractants =" ::
+ map (Display.string_of_thm_global thy) extractants))
else ()
val TCs = List.foldr (gen_union (op aconv)) [] TCl
val full_rqt = WFR::TCs
@@ -551,8 +550,9 @@
|> PureThy.add_defs false
[Thm.no_attributes (Binding.name (fid ^ "_def"), defn)]
val def = Thm.freezeT def0;
- val dummy = if !trace then writeln ("DEF = " ^ Display.string_of_thm def)
- else ()
+ val dummy =
+ if !trace then writeln ("DEF = " ^ Display.string_of_thm_global theory def)
+ else ()
(* val fconst = #lhs(S.dest_eq(concl def)) *)
val tych = Thry.typecheck theory
val full_rqt_prop = map (Dcterm.mk_prop o tych) full_rqt
@@ -560,7 +560,7 @@
val baz = R.DISCH_ALL
(fold_rev R.DISCH full_rqt_prop
(R.LIST_CONJ extractants))
- val dum = if !trace then writeln ("baz = " ^ Display.string_of_thm baz)
+ val dum = if !trace then writeln ("baz = " ^ Display.string_of_thm_global theory baz)
else ()
val f_free = Free (fid, fastype_of f) (*'cos f is a Const*)
val SV' = map tych SV;
@@ -909,7 +909,7 @@
fun trace_thms s L =
- if !trace then writeln (cat_lines (s :: map Display.string_of_thm L))
+ if !trace then writeln (cat_lines (s :: map Display.string_of_thm_without_context L))
else ();
fun trace_cterms s L =
--- a/src/HOL/Tools/atp_minimal.ML Tue Jul 21 00:56:19 2009 +0200
+++ b/src/HOL/Tools/atp_minimal.ML Tue Jul 21 01:03:18 2009 +0200
@@ -125,7 +125,8 @@
println ("Minimize called with " ^ length_string name_thms_pairs ^ " theorems, prover: "
^ prover_name ^ ", time limit: " ^ Int.toString time_limit ^ " seconds")
val _ = debug_fn (fn () => app (fn (n, tl) =>
- (debug n; app (fn t => debug (" " ^ Display.string_of_thm t)) tl)) name_thms_pairs)
+ (debug n; app (fn t =>
+ debug (" " ^ Display.string_of_thm (Proof.context_of state) t)) tl)) name_thms_pairs)
val test_thms_fun = sh_test_thms prover prover_name time_limit 1 state
fun test_thms filtered thms =
case test_thms_fun filtered thms of (Success _, _) => true | _ => false
--- a/src/HOL/Tools/atp_wrapper.ML Tue Jul 21 00:56:19 2009 +0200
+++ b/src/HOL/Tools/atp_wrapper.ML Tue Jul 21 01:03:18 2009 +0200
@@ -62,7 +62,7 @@
val goal_cls = #1 (ResAxioms.neg_conjecture_clauses th subgoalno)
handle THM ("assume: variables", _, _) =>
error "Sledgehammer: Goal contains type variables (TVars)"
- val _ = app (fn th => Output.debug (fn _ => Display.string_of_thm th)) goal_cls
+ val _ = app (fn th => Output.debug (fn _ => Display.string_of_thm ctxt th)) goal_cls
val the_filtered_clauses =
case filtered_clauses of
NONE => relevance_filter goal goal_cls
--- a/src/HOL/Tools/choice_specification.ML Tue Jul 21 00:56:19 2009 +0200
+++ b/src/HOL/Tools/choice_specification.ML Tue Jul 21 01:03:18 2009 +0200
@@ -183,7 +183,7 @@
fun add_final (arg as (thy, thm)) =
if name = ""
then arg |> Library.swap
- else (writeln (" " ^ name ^ ": " ^ (Display.string_of_thm thm));
+ else (writeln (" " ^ name ^ ": " ^ Display.string_of_thm_global thy thm);
PureThy.store_thm (Binding.name name, thm) thy)
in
args |> apsnd (remove_alls frees)
--- a/src/HOL/Tools/inductive.ML Tue Jul 21 00:56:19 2009 +0200
+++ b/src/HOL/Tools/inductive.ML Tue Jul 21 01:03:18 2009 +0200
@@ -140,7 +140,7 @@
val space = Consts.space_of (ProofContext.consts_of ctxt);
in
[Pretty.strs ("(co)inductives:" :: map #1 (NameSpace.extern_table (space, tab))),
- Pretty.big_list "monotonicity rules:" (map (ProofContext.pretty_thm ctxt) monos)]
+ Pretty.big_list "monotonicity rules:" (map (Display.pretty_thm ctxt) monos)]
|> Pretty.chunks |> Pretty.writeln
end;
@@ -179,7 +179,8 @@
[dest_less_concl (Seq.hd (REPEAT (FIRSTGOAL
(resolve_tac [le_funI, le_boolI'])) thm))]
| _ => [thm]
- end handle THM _ => error ("Bad monotonicity theorem:\n" ^ Display.string_of_thm thm);
+ end handle THM _ =>
+ error ("Bad monotonicity theorem:\n" ^ Display.string_of_thm_without_context thm);
val mono_add = Thm.declaration_attribute (map_monos o fold Thm.add_thm o mk_mono);
val mono_del = Thm.declaration_attribute (map_monos o fold Thm.del_thm o mk_mono);
--- a/src/HOL/Tools/inductive_codegen.ML Tue Jul 21 00:56:19 2009 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML Tue Jul 21 01:03:18 2009 +0200
@@ -39,7 +39,7 @@
fun warn thm = warning ("InductiveCodegen: Not a proper clause:\n" ^
- Display.string_of_thm thm);
+ Display.string_of_thm_without_context thm);
fun add_node (g, x) = Graph.new_node (x, ()) g handle Graph.DUP _ => g;
--- a/src/HOL/Tools/inductive_realizer.ML Tue Jul 21 00:56:19 2009 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML Tue Jul 21 01:03:18 2009 +0200
@@ -19,7 +19,7 @@
(case Proofterm.fold_proof_atoms false (fn PThm (_, ((name, _, _), _)) => cons name | _ => I)
[Thm.proof_of thm] [] of
[name] => name
- | _ => error ("name_of_thm: bad proof of theorem\n" ^ Display.string_of_thm thm));
+ | _ => error ("name_of_thm: bad proof of theorem\n" ^ Display.string_of_thm_without_context thm));
val all_simps = map (symmetric o mk_meta_eq) (thms "HOL.all_simps");
--- a/src/HOL/Tools/lin_arith.ML Tue Jul 21 00:56:19 2009 +0200
+++ b/src/HOL/Tools/lin_arith.ML Tue Jul 21 01:03:18 2009 +0200
@@ -286,7 +286,7 @@
(* checks if splitting with 'thm' is implemented *)
-fun is_split_thm (thm : thm) : bool =
+fun is_split_thm thm =
case concl_of thm of _ $ (_ $ (_ $ lhs) $ _) => (
(* Trueprop $ ((op =) $ (?P $ lhs) $ rhs) *)
case head_of lhs of
@@ -298,10 +298,10 @@
"Divides.div_class.mod",
"Divides.div_class.div"] a
| _ => (warning ("Lin. Arith.: wrong format for split rule " ^
- Display.string_of_thm thm);
+ Display.string_of_thm_without_context thm);
false))
| _ => (warning ("Lin. Arith.: wrong format for split rule " ^
- Display.string_of_thm thm);
+ Display.string_of_thm_without_context thm);
false);
(* substitute new for occurrences of old in a term, incrementing bound *)
--- a/src/HOL/Tools/meson.ML Tue Jul 21 00:56:19 2009 +0200
+++ b/src/HOL/Tools/meson.ML Tue Jul 21 01:03:18 2009 +0200
@@ -127,10 +127,10 @@
fun forward_res nf st =
let fun forward_tacf [prem] = rtac (nf prem) 1
| forward_tacf prems =
- error ("Bad proof state in forward_res, please inform lcp@cl.cam.ac.uk:\n" ^
- Display.string_of_thm st ^
- "\nPremises:\n" ^
- ML_Syntax.print_list Display.string_of_thm prems)
+ error (cat_lines
+ ("Bad proof state in forward_res, please inform lcp@cl.cam.ac.uk:" ::
+ Display.string_of_thm_without_context st ::
+ "Premises:" :: map Display.string_of_thm_without_context prems))
in
case Seq.pull (ALLGOALS (METAHYPS forward_tacf) st)
of SOME(th,_) => th
@@ -342,7 +342,7 @@
and cnf_nil th = cnf_aux (th,[])
val cls =
if too_many_clauses (SOME ctxt) (concl_of th)
- then (warning ("cnf is ignoring: " ^ Display.string_of_thm th); ths)
+ then (warning ("cnf is ignoring: " ^ Display.string_of_thm ctxt th); ths)
else cnf_aux (th,ths)
in (cls, !ctxtr) end;
@@ -545,7 +545,7 @@
| skolemize_nnf_list (th::ths) =
skolemize th :: skolemize_nnf_list ths
handle THM _ => (*RS can fail if Unify.search_bound is too small*)
- (warning ("Failed to Skolemize " ^ Display.string_of_thm th);
+ (warning ("Failed to Skolemize " ^ Display.string_of_thm_without_context th);
skolemize_nnf_list ths);
fun add_clauses (th,cls) =
@@ -628,19 +628,17 @@
ITER_DEEPEN (has_fewer_prems 1) (prolog_step_tac' horns);
fun iter_deepen_meson_tac ths = MESON make_clauses
- (fn cls =>
- case (gocls (cls@ths)) of
- [] => no_tac (*no goal clauses*)
- | goes =>
- let val horns = make_horns (cls@ths)
- val _ =
- Output.debug (fn () => ("meson method called:\n" ^
- ML_Syntax.print_list Display.string_of_thm (cls@ths) ^
- "\nclauses:\n" ^
- ML_Syntax.print_list Display.string_of_thm horns))
- in THEN_ITER_DEEPEN (resolve_tac goes 1) (has_fewer_prems 1) (prolog_step_tac' horns)
- end
- );
+ (fn cls =>
+ (case (gocls (cls @ ths)) of
+ [] => no_tac (*no goal clauses*)
+ | goes =>
+ let
+ val horns = make_horns (cls @ ths)
+ val _ = Output.debug (fn () =>
+ cat_lines ("meson method called:" ::
+ map Display.string_of_thm_without_context (cls @ ths) @
+ ["clauses:"] @ map Display.string_of_thm_without_context horns))
+ in THEN_ITER_DEEPEN (resolve_tac goes 1) (has_fewer_prems 1) (prolog_step_tac' horns) end));
fun meson_claset_tac ths cs =
SELECT_GOAL (TRY (safe_tac cs) THEN TRYALL (iter_deepen_meson_tac ths));
--- a/src/HOL/Tools/metis_tools.ML Tue Jul 21 00:56:19 2009 +0200
+++ b/src/HOL/Tools/metis_tools.ML Tue Jul 21 01:03:18 2009 +0200
@@ -270,7 +270,7 @@
fun print_thpair (fth,th) =
(Output.debug (fn () => "=============================================");
Output.debug (fn () => "Metis: " ^ Metis.Thm.toString fth);
- Output.debug (fn () => "Isabelle: " ^ Display.string_of_thm th));
+ Output.debug (fn () => "Isabelle: " ^ Display.string_of_thm_without_context th));
fun lookth thpairs (fth : Metis.Thm.thm) =
valOf (AList.lookup (uncurry Metis.Thm.equal) thpairs fth)
@@ -310,7 +310,7 @@
in SOME (cterm_of thy (Var v), t) end
handle Option =>
(Output.debug (fn() => "List.find failed for the variable " ^ x ^
- " in " ^ Display.string_of_thm i_th);
+ " in " ^ Display.string_of_thm ctxt i_th);
NONE)
fun remove_typeinst (a, t) =
case Recon.strip_prefix ResClause.schematic_var_prefix a of
@@ -318,7 +318,7 @@
| NONE => case Recon.strip_prefix ResClause.tvar_prefix a of
SOME _ => NONE (*type instantiations are forbidden!*)
| NONE => SOME (a,t) (*internal Metis var?*)
- val _ = Output.debug (fn () => " isa th: " ^ Display.string_of_thm i_th)
+ val _ = Output.debug (fn () => " isa th: " ^ Display.string_of_thm ctxt i_th)
val substs = List.mapPartial remove_typeinst (Metis.Subst.toList fsubst)
val (vars,rawtms) = ListPair.unzip (List.mapPartial subst_translation substs)
val tms = infer_types ctxt rawtms;
@@ -350,8 +350,8 @@
let
val thy = ProofContext.theory_of ctxt
val i_th1 = lookth thpairs th1 and i_th2 = lookth thpairs th2
- val _ = Output.debug (fn () => " isa th1 (pos): " ^ Display.string_of_thm i_th1)
- val _ = Output.debug (fn () => " isa th2 (neg): " ^ Display.string_of_thm i_th2)
+ val _ = Output.debug (fn () => " isa th1 (pos): " ^ Display.string_of_thm ctxt i_th1)
+ val _ = Output.debug (fn () => " isa th2 (neg): " ^ Display.string_of_thm ctxt i_th2)
in
if is_TrueI i_th1 then i_th2 (*Trivial cases where one operand is type info*)
else if is_TrueI i_th2 then i_th1
@@ -428,7 +428,7 @@
val _ = Output.debug (fn () => "located term: " ^ Syntax.string_of_term ctxt tm_subst)
val imax = maxidx_of_term (i_tm $ tm_abs $ tm_subst) (*ill typed but gives right max*)
val subst' = incr_indexes (imax+1) (if pos then subst_em else ssubst_em)
- val _ = Output.debug (fn () => "subst' " ^ Display.string_of_thm subst')
+ val _ = Output.debug (fn () => "subst' " ^ Display.string_of_thm ctxt subst')
val eq_terms = map (pairself (cterm_of thy))
(ListPair.zip (OldTerm.term_vars (prop_of subst'), [tm_abs, tm_subst, i_tm]))
in cterm_instantiate eq_terms subst' end;
@@ -456,7 +456,7 @@
val _ = Output.debug (fn () => "METIS THM: " ^ Metis.Thm.toString fol_th)
val _ = Output.debug (fn () => "INFERENCE: " ^ Metis.Proof.inferenceToString inf)
val th = Meson.flexflex_first_order (step ctxt isFO thpairs (fol_th, inf))
- val _ = Output.debug (fn () => "ISABELLE THM: " ^ Display.string_of_thm th)
+ val _ = Output.debug (fn () => "ISABELLE THM: " ^ Display.string_of_thm ctxt th)
val _ = Output.debug (fn () => "=============================================")
val n_metis_lits = length (filter real_literal (Metis.LiteralSet.toList (Metis.Thm.clause fol_th)))
in
@@ -576,9 +576,9 @@
val th_cls_pairs = map (fn th => (Thm.get_name_hint th, ResAxioms.cnf_axiom thy th)) ths0
val ths = List.concat (map #2 th_cls_pairs)
val _ = Output.debug (fn () => "FOL_SOLVE: CONJECTURE CLAUSES")
- val _ = app (fn th => Output.debug (fn () => Display.string_of_thm th)) cls
+ val _ = app (fn th => Output.debug (fn () => Display.string_of_thm ctxt th)) cls
val _ = Output.debug (fn () => "THEOREM CLAUSES")
- val _ = app (fn th => Output.debug (fn () => Display.string_of_thm th)) ths
+ val _ = app (fn th => Output.debug (fn () => Display.string_of_thm ctxt th)) ths
val {isFO,axioms,tfrees} = build_map mode ctxt cls ths
val _ = if null tfrees then ()
else (Output.debug (fn () => "TFREE CLAUSES");
@@ -604,14 +604,14 @@
val result = translate isFO ctxt' axioms proof
and used = List.mapPartial (used_axioms axioms) proof
val _ = Output.debug (fn () => "METIS COMPLETED...clauses actually used:")
- val _ = app (fn th => Output.debug (fn () => Display.string_of_thm th)) used
+ val _ = app (fn th => Output.debug (fn () => Display.string_of_thm ctxt th)) used
val unused = filter (fn (a,cls) => not (common_thm used cls)) th_cls_pairs
in
if null unused then ()
else warning ("Metis: unused theorems " ^ commas_quote (map #1 unused));
case result of
(_,ith)::_ =>
- (Output.debug (fn () => "success: " ^ Display.string_of_thm ith);
+ (Output.debug (fn () => "success: " ^ Display.string_of_thm ctxt ith);
[ith])
| _ => (Output.debug (fn () => "Metis: no result");
[])
@@ -623,7 +623,7 @@
fun metis_general_tac mode ctxt ths i st0 =
let val _ = Output.debug (fn () =>
- "Metis called with theorems " ^ cat_lines (map Display.string_of_thm ths))
+ "Metis called with theorems " ^ cat_lines (map (Display.string_of_thm ctxt) ths))
in
if exists_type ResAxioms.type_has_empty_sort (prop_of st0)
then (warning "Proof state contains the empty sort"; Seq.empty)
--- a/src/HOL/Tools/recdef.ML Tue Jul 21 00:56:19 2009 +0200
+++ b/src/HOL/Tools/recdef.ML Tue Jul 21 01:03:18 2009 +0200
@@ -48,9 +48,9 @@
fun map_wfs f = map_hints (fn (simps, congs, wfs) => (simps, congs, f wfs));
fun pretty_hints ({simps, congs, wfs}: hints) =
- [Pretty.big_list "recdef simp hints:" (map Display.pretty_thm simps),
- Pretty.big_list "recdef cong hints:" (map Display.pretty_thm (map snd congs)),
- Pretty.big_list "recdef wf hints:" (map Display.pretty_thm wfs)];
+ [Pretty.big_list "recdef simp hints:" (map Display.pretty_thm_without_context simps),
+ Pretty.big_list "recdef cong hints:" (map Display.pretty_thm_without_context (map snd congs)),
+ Pretty.big_list "recdef wf hints:" (map Display.pretty_thm_without_context wfs)];
(* congruence rules *)
--- a/src/HOL/Tools/record.ML Tue Jul 21 00:56:19 2009 +0200
+++ b/src/HOL/Tools/record.ML Tue Jul 21 01:03:18 2009 +0200
@@ -105,7 +105,7 @@
(* messages *)
fun trace_thm str thm =
- tracing (str ^ (Pretty.string_of (Display.pretty_thm thm)));
+ tracing (str ^ (Pretty.string_of (Display.pretty_thm_without_context thm)));
fun trace_thms str thms =
(tracing str; map (trace_thm "") thms);
--- a/src/HOL/Tools/res_atp.ML Tue Jul 21 00:56:19 2009 +0200
+++ b/src/HOL/Tools/res_atp.ML Tue Jul 21 01:03:18 2009 +0200
@@ -401,8 +401,9 @@
(List.foldl add_single_names (List.foldl add_multi_names [] mults) singles)
end;
-fun check_named ("",th) = (warning ("No name for theorem " ^ Display.string_of_thm th); false)
- | check_named (_,th) = true;
+fun check_named ("", th) =
+ (warning ("No name for theorem " ^ Display.string_of_thm_without_context th); false)
+ | check_named (_, th) = true;
(* get lemmas from claset, simpset, atpset and extra supplied rules *)
fun get_clasimp_atp_lemmas ctxt =
@@ -538,7 +539,7 @@
val extra_cls = white_cls @ extra_cls
val axcls = white_cls @ axcls
val ccls = subtract_cls goal_cls extra_cls
- val _ = app (fn th => Output.debug (fn _ => Display.string_of_thm th)) ccls
+ val _ = app (fn th => Output.debug (fn _ => Display.string_of_thm_global thy th)) ccls
val ccltms = map prop_of ccls
and axtms = map (prop_of o #1) extra_cls
val subs = tfree_classes_of_terms ccltms
--- a/src/HOL/Tools/res_axioms.ML Tue Jul 21 00:56:19 2009 +0200
+++ b/src/HOL/Tools/res_axioms.ML Tue Jul 21 01:03:18 2009 +0200
@@ -227,8 +227,9 @@
val eqth = combinators_aux (cprop_of th)
in equal_elim eqth th end
handle THM (msg,_,_) =>
- (warning ("Error in the combinator translation of " ^ Display.string_of_thm th);
- warning (" Exception message: " ^ msg);
+ (warning (cat_lines
+ ["Error in the combinator translation of " ^ Display.string_of_thm_without_context th,
+ " Exception message: " ^ msg]);
TrueI); (*A type variable of sort {} will cause make abstraction fail.*)
(*cterms are used throughout for efficiency*)
@@ -280,7 +281,7 @@
fun assert_lambda_free ths msg =
case filter (not o lambda_free o prop_of) ths of
[] => ()
- | ths' => error (msg ^ "\n" ^ cat_lines (map Display.string_of_thm ths'));
+ | ths' => error (cat_lines (msg :: map Display.string_of_thm_without_context ths'));
(*** Blacklisting (duplicated in ResAtp?) ***)
@@ -336,7 +337,7 @@
fun name_or_string th =
if Thm.has_name_hint th then Thm.get_name_hint th
- else Display.string_of_thm th;
+ else Display.string_of_thm_without_context th;
(*Skolemize a named theorem, with Skolem functions as additional premises.*)
fun skolem_thm (s, th) =
--- a/src/HOL/Tools/res_reconstruct.ML Tue Jul 21 00:56:19 2009 +0200
+++ b/src/HOL/Tools/res_reconstruct.ML Tue Jul 21 01:03:18 2009 +0200
@@ -31,7 +31,7 @@
fun trace s = if !Output.debugging then File.append (File.tmp_path trace_path) s
else ();
-val string_of_thm = PrintMode.setmp [] Display.string_of_thm;
+fun string_of_thm ctxt = PrintMode.setmp [] (Display.string_of_thm ctxt);
(*For generating structured proofs: keep every nth proof line*)
val (modulus, modulus_setup) = Attrib.config_int "sledgehammer_modulus" 1;
@@ -445,8 +445,9 @@
val (ccls,fixes) = ResAxioms.neg_conjecture_clauses th sgno
val _ = trace (Int.toString (length ccls) ^ " conjecture clauses\n")
val ccls = map forall_intr_vars ccls
- val _ = if !Output.debugging then app (fn th => trace ("\nccl: " ^ string_of_thm th)) ccls
- else ()
+ val _ =
+ if !Output.debugging then app (fn th => trace ("\nccl: " ^ string_of_thm ctxt th)) ccls
+ else ()
val ilines = isar_lines ctxt (map prop_of ccls) (stringify_deps thm_names [] lines)
val _ = trace "\ndecode_tstp_file: finishing\n"
in
--- a/src/HOL/Tools/sat_funcs.ML Tue Jul 21 00:56:19 2009 +0200
+++ b/src/HOL/Tools/sat_funcs.ML Tue Jul 21 01:03:18 2009 +0200
@@ -119,7 +119,7 @@
(* (Thm.thm * (int * Thm.cterm) list) list -> Thm.thm * (int * Thm.cterm) list *)
fun resolve_raw_clauses [] =
- raise THM ("Proof reconstruction failed (empty list of resolvents)!", 0, [])
+ raise THM ("Proof reconstruction failed (empty list of resolvents)!", 0, [])
| resolve_raw_clauses (c::cs) =
let
(* merges two sorted lists wrt. 'lit_ord', suppressing duplicates *)
@@ -134,9 +134,9 @@
(* find out which two hyps are used in the resolution *)
(* (int * Thm.cterm) list * (int * Thm.cterm) list -> (int * Thm.cterm) list -> bool * Thm.cterm * Thm.cterm * (int * Thm.cterm) list *)
fun find_res_hyps ([], _) _ =
- raise THM ("Proof reconstruction failed (no literal for resolution)!", 0, [])
+ raise THM ("Proof reconstruction failed (no literal for resolution)!", 0, [])
| find_res_hyps (_, []) _ =
- raise THM ("Proof reconstruction failed (no literal for resolution)!", 0, [])
+ raise THM ("Proof reconstruction failed (no literal for resolution)!", 0, [])
| find_res_hyps (h1 :: hyps1, h2 :: hyps2) acc =
(case (lit_ord o pairself fst) (h1, h2) of
LESS => find_res_hyps (hyps1, h2 :: hyps2) (h1 :: acc)
@@ -154,9 +154,12 @@
(* Thm.thm * (int * Thm.cterm) list -> Thm.thm * (int * Thm.cterm) list -> Thm.thm * (int * Thm.cterm) list *)
fun resolution (c1, hyps1) (c2, hyps2) =
let
- val _ = if !trace_sat then
- 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))
- ^ ")\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)) ^ ")")
+ val _ =
+ if ! trace_sat then
+ tracing ("Resolving clause: " ^ Display.string_of_thm_without_context c1 ^
+ " (hyps: " ^ ML_Syntax.print_list (Syntax.string_of_term_global (theory_of_thm c1)) (#hyps (rep_thm c1))
+ ^ ")\nwith clause: " ^ Display.string_of_thm_without_context c2 ^
+ " (hyps: " ^ ML_Syntax.print_list (Syntax.string_of_term_global (theory_of_thm c2)) (#hyps (rep_thm c2)) ^ ")")
else ()
(* the two literals used for resolution *)
@@ -172,8 +175,9 @@
Thm.instantiate ([], [(cP, cLit)]) resolution_thm
end
- val _ = if !trace_sat then
- tracing ("Resolution theorem: " ^ Display.string_of_thm res_thm)
+ val _ =
+ if !trace_sat then
+ tracing ("Resolution theorem: " ^ Display.string_of_thm_without_context res_thm)
else ()
(* Gamma1, Gamma2 |- False *)
@@ -181,8 +185,11 @@
(Thm.implies_elim res_thm (if hyp1_is_neg then c2' else c1'))
(if hyp1_is_neg then c1' else c2')
- val _ = if !trace_sat then
- 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)) ^ ")")
+ val _ =
+ if !trace_sat then
+ tracing ("Resulting clause: " ^ Display.string_of_thm_without_context c_new ^
+ " (hyps: " ^ ML_Syntax.print_list
+ (Syntax.string_of_term_global (theory_of_thm c_new)) (#hyps (rep_thm c_new)) ^ ")")
else ()
val _ = inc counter
in
--- a/src/HOL/ex/predicate_compile.ML Tue Jul 21 00:56:19 2009 +0200
+++ b/src/HOL/ex/predicate_compile.ML Tue Jul 21 01:03:18 2009 +0200
@@ -236,11 +236,11 @@
val _ = writeln ("predicate: " ^ pred)
val _ = writeln ("number of parameters: " ^ string_of_int (nparams_of thy pred))
val _ = writeln ("introrules: ")
- val _ = fold (fn thm => fn u => writeln (Display.string_of_thm thm))
+ val _ = fold (fn thm => fn u => writeln (Display.string_of_thm_global thy thm))
(rev (intros_of thy pred)) ()
in
if (has_elim thy pred) then
- writeln ("elimrule: " ^ Display.string_of_thm (the_elim_of thy pred))
+ writeln ("elimrule: " ^ Display.string_of_thm_global thy (the_elim_of thy pred))
else
writeln ("no elimrule defined")
end
--- a/src/Provers/Arith/fast_lin_arith.ML Tue Jul 21 00:56:19 2009 +0200
+++ b/src/Provers/Arith/fast_lin_arith.ML Tue Jul 21 01:03:18 2009 +0200
@@ -417,8 +417,8 @@
(* Translate back a proof. *)
(* ------------------------------------------------------------------------- *)
-fun trace_thm msg th =
- (if !trace then (tracing msg; tracing (Display.string_of_thm th)) else (); th);
+fun trace_thm ctxt msg th =
+ (if !trace then (tracing msg; tracing (Display.string_of_thm ctxt th)) else (); th);
fun trace_term ctxt msg t =
(if !trace then tracing (cat_lines [msg, Syntax.string_of_term ctxt t]) else (); t)
@@ -472,7 +472,7 @@
NONE =>
(the (try_add ([thm2] RL inj_thms) thm1)
handle Option =>
- (trace_thm "" thm1; trace_thm "" thm2;
+ (trace_thm ctxt "" thm1; trace_thm ctxt "" thm2;
sys_error "Linear arithmetic: failed to add thms"))
| SOME thm => thm)
| SOME thm => thm);
@@ -511,24 +511,25 @@
else mult n thm;
fun simp thm =
- let val thm' = trace_thm "Simplified:" (full_simplify simpset' thm)
+ let val thm' = trace_thm ctxt "Simplified:" (full_simplify simpset' thm)
in if LA_Logic.is_False thm' then raise FalseE thm' else thm' end;
- fun mk (Asm i) = trace_thm ("Asm " ^ string_of_int i) (nth asms i)
- | mk (Nat i) = trace_thm ("Nat " ^ string_of_int i) (LA_Logic.mk_nat_thm thy (nth atoms i))
- | mk (LessD j) = trace_thm "L" (hd ([mk j] RL lessD))
- | mk (NotLeD j) = trace_thm "NLe" (mk j RS LA_Logic.not_leD)
- | mk (NotLeDD j) = trace_thm "NLeD" (hd ([mk j RS LA_Logic.not_leD] RL lessD))
- | mk (NotLessD j) = trace_thm "NL" (mk j RS LA_Logic.not_lessD)
- | mk (Added (j1, j2)) = simp (trace_thm "+" (add_thms (mk j1) (mk j2)))
- | mk (Multiplied (n, j)) = (trace_msg ("*" ^ string_of_int n); trace_thm "*" (mult_thm (n, mk j)))
+ fun mk (Asm i) = trace_thm ctxt ("Asm " ^ string_of_int i) (nth asms i)
+ | mk (Nat i) = trace_thm ctxt ("Nat " ^ string_of_int i) (LA_Logic.mk_nat_thm thy (nth atoms i))
+ | mk (LessD j) = trace_thm ctxt "L" (hd ([mk j] RL lessD))
+ | mk (NotLeD j) = trace_thm ctxt "NLe" (mk j RS LA_Logic.not_leD)
+ | mk (NotLeDD j) = trace_thm ctxt "NLeD" (hd ([mk j RS LA_Logic.not_leD] RL lessD))
+ | mk (NotLessD j) = trace_thm ctxt "NL" (mk j RS LA_Logic.not_lessD)
+ | mk (Added (j1, j2)) = simp (trace_thm ctxt "+" (add_thms (mk j1) (mk j2)))
+ | mk (Multiplied (n, j)) =
+ (trace_msg ("*" ^ string_of_int n); trace_thm ctxt "*" (mult_thm (n, mk j)))
in
let
val _ = trace_msg "mkthm";
- val thm = trace_thm "Final thm:" (mk just);
+ val thm = trace_thm ctxt "Final thm:" (mk just);
val fls = simplify simpset' thm;
- val _ = trace_thm "After simplification:" fls;
+ val _ = trace_thm ctxt "After simplification:" fls;
val _ =
if LA_Logic.is_False fls then ()
else
@@ -536,15 +537,15 @@
if count > warning_count_max then ()
else
(tracing (cat_lines
- (["Assumptions:"] @ map Display.string_of_thm asms @ [""] @
- ["Proved:", Display.string_of_thm fls, ""] @
+ (["Assumptions:"] @ map (Display.string_of_thm ctxt) asms @ [""] @
+ ["Proved:", Display.string_of_thm ctxt fls, ""] @
(if count <> warning_count_max then []
else ["\n(Reached maximal message count -- disabling future warnings)"])));
warning "Linear arithmetic should have refuted the assumptions.\n\
\Please inform Tobias Nipkow (nipkow@in.tum.de).")
end;
in fls end
- handle FalseE thm => trace_thm "False reached early:" thm
+ handle FalseE thm => trace_thm ctxt "False reached early:" thm
end;
end;
@@ -775,8 +776,9 @@
fn state =>
let
val ctxt = Simplifier.the_context ss;
- val _ = trace_thm ("refute_tac (on subgoal " ^ string_of_int i ^ ", with " ^
- string_of_int (length justs) ^ " justification(s)):") state
+ val _ = trace_thm ctxt
+ ("refute_tac (on subgoal " ^ string_of_int i ^ ", with " ^
+ string_of_int (length justs) ^ " justification(s)):") state
val {neqE, ...} = get_data ctxt;
fun just1 j =
(* eliminate inequalities *)
@@ -784,7 +786,7 @@
REPEAT_DETERM (eresolve_tac neqE i)
else
all_tac) THEN
- PRIMITIVE (trace_thm "State after neqE:") THEN
+ PRIMITIVE (trace_thm ctxt "State after neqE:") THEN
(* use theorems generated from the actual justifications *)
METAHYPS (fn asms => rtac (mkthm ss asms j) 1) i
in
@@ -792,7 +794,7 @@
DETERM (resolve_tac [LA_Logic.notI, LA_Logic.ccontr] i) THEN
(* user-defined preprocessing of the subgoal *)
DETERM (LA_Data.pre_tac ctxt i) THEN
- PRIMITIVE (trace_thm "State after pre_tac:") THEN
+ PRIMITIVE (trace_thm ctxt "State after pre_tac:") THEN
(* prove every resulting subgoal, using its justification *)
EVERY (map just1 justs)
end state;
@@ -881,7 +883,7 @@
val (Falsethm, _) = fwdproof ss tree js
val contr = if pos then LA_Logic.ccontr else LA_Logic.notI
val concl = implies_intr cnTconcl Falsethm COMP contr
- in SOME (trace_thm "Proved by lin. arith. prover:" (LA_Logic.mk_Eq concl)) end
+ in SOME (trace_thm ctxt "Proved by lin. arith. prover:" (LA_Logic.mk_Eq concl)) end
(*in case concl contains ?-var, which makes assume fail:*) (* FIXME Variable.import_terms *)
handle THM _ => NONE;
--- a/src/Provers/blast.ML Tue Jul 21 00:56:19 2009 +0200
+++ b/src/Provers/blast.ML Tue Jul 21 01:03:18 2009 +0200
@@ -492,7 +492,9 @@
end;
-fun TRACE rl tac st i = if !trace then (Display.prth rl; tac st i) else tac st i;
+fun TRACE rl tac st i =
+ if !trace then (writeln (Display.string_of_thm_without_context rl); tac st i)
+ else tac st i;
(*Resolution/matching tactics: if upd then the proof state may be updated.
Matching makes the tactics more deterministic in the presence of Vars.*)
@@ -509,14 +511,16 @@
THEN
rot_subgoals_tac (rot, #2 trl) i
in Option.SOME (trl, tac) end
- handle ElimBadPrem => (*reject: prems don't preserve conclusion*)
- (warning("Ignoring weak elimination rule\n" ^ Display.string_of_thm rl);
- Option.NONE)
- | ElimBadConcl => (*ignore: conclusion is not just a variable*)
- (if !trace then (warning("Ignoring ill-formed elimination rule:\n" ^
- "conclusion should be a variable\n" ^ Display.string_of_thm rl))
- else ();
- Option.NONE);
+ handle
+ ElimBadPrem => (*reject: prems don't preserve conclusion*)
+ (warning ("Ignoring weak elimination rule\n" ^ Display.string_of_thm_global thy rl);
+ Option.NONE)
+ | ElimBadConcl => (*ignore: conclusion is not just a variable*)
+ (if !trace then
+ (warning ("Ignoring ill-formed elimination rule:\n" ^
+ "conclusion should be a variable\n" ^ Display.string_of_thm_global thy rl))
+ else ();
+ Option.NONE);
(*** Conversion of Introduction Rules ***)
--- a/src/Provers/classical.ML Tue Jul 21 00:56:19 2009 +0200
+++ b/src/Provers/classical.ML Tue Jul 21 01:03:18 2009 +0200
@@ -256,7 +256,7 @@
xtra_netpair = empty_netpair};
fun print_cs (CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, ...}) =
- let val pretty_thms = map Display.pretty_thm in
+ let val pretty_thms = map Display.pretty_thm_without_context in
[Pretty.big_list "safe introduction rules (intro!):" (pretty_thms safeIs),
Pretty.big_list "introduction rules (intro):" (pretty_thms hazIs),
Pretty.big_list "safe elimination rules (elim!):" (pretty_thms safeEs),
@@ -313,14 +313,18 @@
(*Warn if the rule is already present ELSEWHERE in the claset. The addition
is still allowed.*)
fun warn_dup th (CS{safeIs, safeEs, hazIs, hazEs, ...}) =
- if mem_thm safeIs th then
- warning ("Rule already declared as safe introduction (intro!)\n" ^ Display.string_of_thm th)
+ if mem_thm safeIs th then
+ warning ("Rule already declared as safe introduction (intro!)\n" ^
+ Display.string_of_thm_without_context th)
else if mem_thm safeEs th then
- warning ("Rule already declared as safe elimination (elim!)\n" ^ Display.string_of_thm th)
+ warning ("Rule already declared as safe elimination (elim!)\n" ^
+ Display.string_of_thm_without_context th)
else if mem_thm hazIs th then
- warning ("Rule already declared as introduction (intro)\n" ^ Display.string_of_thm th)
+ warning ("Rule already declared as introduction (intro)\n" ^
+ Display.string_of_thm_without_context th)
else if mem_thm hazEs th then
- warning ("Rule already declared as elimination (elim)\n" ^ Display.string_of_thm th)
+ warning ("Rule already declared as elimination (elim)\n" ^
+ Display.string_of_thm_without_context th)
else ();
@@ -330,8 +334,8 @@
(cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
if mem_thm safeIs th then
- (warning ("Ignoring duplicate safe introduction (intro!)\n" ^ Display.string_of_thm th);
- cs)
+ (warning ("Ignoring duplicate safe introduction (intro!)\n" ^
+ Display.string_of_thm_without_context th); cs)
else
let val th' = flat_rule th
val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*)
@@ -356,10 +360,10 @@
(cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
if mem_thm safeEs th then
- (warning ("Ignoring duplicate safe elimination (elim!)\n" ^ Display.string_of_thm th);
- cs)
+ (warning ("Ignoring duplicate safe elimination (elim!)\n" ^
+ Display.string_of_thm_without_context th); cs)
else if has_fewer_prems 1 th then
- error("Ill-formed elimination rule\n" ^ Display.string_of_thm th)
+ error ("Ill-formed elimination rule\n" ^ Display.string_of_thm_without_context th)
else
let
val th' = classical_rule (flat_rule th)
@@ -386,7 +390,7 @@
fun make_elim th =
if has_fewer_prems 1 th then
- error("Ill-formed destruction rule\n" ^ Display.string_of_thm th)
+ error ("Ill-formed destruction rule\n" ^ Display.string_of_thm_without_context th)
else Tactic.make_elim th;
fun cs addSDs ths = cs addSEs (map make_elim ths);
@@ -398,8 +402,8 @@
(cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
if mem_thm hazIs th then
- (warning ("Ignoring duplicate introduction (intro)\n" ^ Display.string_of_thm th);
- cs)
+ (warning ("Ignoring duplicate introduction (intro)\n" ^
+ Display.string_of_thm_without_context th); cs)
else
let val th' = flat_rule th
val nI = length hazIs + 1
@@ -418,16 +422,16 @@
xtra_netpair = insert' (the_default 1 w) (nI,nE) ([th], []) xtra_netpair}
end
handle THM("RSN: no unifiers",_,_) => (*from dup_intr*)
- error ("Ill-formed introduction rule\n" ^ Display.string_of_thm th);
+ error ("Ill-formed introduction rule\n" ^ Display.string_of_thm_without_context th);
fun addE w th
(cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
if mem_thm hazEs th then
- (warning ("Ignoring duplicate elimination (elim)\n" ^ Display.string_of_thm th);
- cs)
+ (warning ("Ignoring duplicate elimination (elim)\n" ^
+ Display.string_of_thm_without_context th); cs)
else if has_fewer_prems 1 th then
- error("Ill-formed elimination rule\n" ^ Display.string_of_thm th)
+ error("Ill-formed elimination rule\n" ^ Display.string_of_thm_without_context th)
else
let
val th' = classical_rule (flat_rule th)
@@ -519,7 +523,7 @@
end
else cs
handle THM("RSN: no unifiers",_,_) => (*from dup_intr*)
- error ("Ill-formed introduction rule\n" ^ Display.string_of_thm th);
+ error ("Ill-formed introduction rule\n" ^ Display.string_of_thm_without_context th);
fun delE th
@@ -548,7 +552,7 @@
mem_thm hazIs th orelse mem_thm hazEs th orelse
mem_thm safeEs th' orelse mem_thm hazEs th'
then delSI th (delSE th (delI th (delE th (delSE th' (delE th' cs)))))
- else (warning ("Undeclared classical rule\n" ^ Display.string_of_thm th); cs)
+ else (warning ("Undeclared classical rule\n" ^ Display.string_of_thm_without_context th); cs)
end;
fun cs delrules ths = fold delrule ths cs;
--- a/src/Pure/Isar/args.ML Tue Jul 21 00:56:19 2009 +0200
+++ b/src/Pure/Isar/args.ML Tue Jul 21 01:03:18 2009 +0200
@@ -88,7 +88,7 @@
fun pretty_src ctxt src =
let
- val prt_thm = Pretty.backquote o ProofContext.pretty_thm ctxt;
+ val prt_thm = Pretty.backquote o Display.pretty_thm ctxt;
fun prt arg =
(case T.get_value arg of
SOME (T.Text s) => Pretty.str (quote s)
--- a/src/Pure/Isar/calculation.ML Tue Jul 21 00:56:19 2009 +0200
+++ b/src/Pure/Isar/calculation.ML Tue Jul 21 01:03:18 2009 +0200
@@ -40,8 +40,8 @@
fun print_rules ctxt =
let val ((trans, sym), _) = CalculationData.get (Context.Proof ctxt) in
[Pretty.big_list "transitivity rules:"
- (map (ProofContext.pretty_thm ctxt) (Item_Net.content trans)),
- Pretty.big_list "symmetry rules:" (map (ProofContext.pretty_thm ctxt) sym)]
+ (map (Display.pretty_thm ctxt) (Item_Net.content trans)),
+ Pretty.big_list "symmetry rules:" (map (Display.pretty_thm ctxt) sym)]
|> Pretty.chunks |> Pretty.writeln
end;
--- a/src/Pure/Isar/code.ML Tue Jul 21 00:56:19 2009 +0200
+++ b/src/Pure/Isar/code.ML Tue Jul 21 01:03:18 2009 +0200
@@ -243,7 +243,7 @@
(*default flag, theorems with proper flag (perhaps lazy)*)
fun pretty_lthms ctxt r = case Lazy.peek r
- of SOME thms => map (ProofContext.pretty_thm ctxt o fst) (Exn.release thms)
+ of SOME thms => map (Display.pretty_thm ctxt o fst) (Exn.release thms)
| NONE => [Pretty.str "[...]"];
fun certificate thy f r =
@@ -263,7 +263,8 @@
Pattern.matchess thy (args, (map incr_idx o curry Library.take (length args)) args');
fun drop (thm', proper') = if (proper orelse not proper')
andalso matches_args (args_of thm') then
- (warning ("Code generator: dropping redundant code equation\n" ^ Display.string_of_thm thm'); true)
+ (warning ("Code generator: dropping redundant code equation\n" ^
+ Display.string_of_thm_global thy thm'); true)
else false;
in (thm, proper) :: filter_out drop thms end;
@@ -567,16 +568,16 @@
fun gen_assert_eqn thy is_constr_pat (thm, proper) =
let
val (lhs, rhs) = (Logic.dest_equals o Thm.plain_prop_of) thm
- handle TERM _ => bad_thm ("Not an equation: " ^ Display.string_of_thm thm)
- | THM _ => bad_thm ("Not an equation: " ^ Display.string_of_thm thm);
+ handle TERM _ => bad_thm ("Not an equation: " ^ Display.string_of_thm_global thy thm)
+ | THM _ => bad_thm ("Not an equation: " ^ Display.string_of_thm_global thy thm);
fun vars_of t = fold_aterms (fn Var (v, _) => insert (op =) v
| Free _ => bad_thm ("Illegal free variable in equation\n"
- ^ Display.string_of_thm thm)
+ ^ Display.string_of_thm_global thy thm)
| _ => I) t [];
fun tvars_of t = fold_term_types (fn _ =>
fold_atyps (fn TVar (v, _) => insert (op =) v
| TFree _ => bad_thm
- ("Illegal free type variable in equation\n" ^ Display.string_of_thm thm))) t [];
+ ("Illegal free type variable in equation\n" ^ Display.string_of_thm_global thy thm))) t [];
val lhs_vs = vars_of lhs;
val rhs_vs = vars_of rhs;
val lhs_tvs = tvars_of lhs;
@@ -584,47 +585,48 @@
val _ = if null (subtract (op =) lhs_vs rhs_vs)
then ()
else bad_thm ("Free variables on right hand side of equation\n"
- ^ Display.string_of_thm thm);
+ ^ Display.string_of_thm_global thy thm);
val _ = if null (subtract (op =) lhs_tvs rhs_tvs)
then ()
else bad_thm ("Free type variables on right hand side of equation\n"
- ^ Display.string_of_thm thm) val (head, args) = (strip_comb o fst o Logic.dest_equals o Thm.plain_prop_of) thm;
+ ^ Display.string_of_thm_global thy thm)
+ val (head, args) = (strip_comb o fst o Logic.dest_equals o Thm.plain_prop_of) thm;
val (c, ty) = case head
of Const (c_ty as (_, ty)) => (AxClass.unoverload_const thy c_ty, ty)
- | _ => bad_thm ("Equation not headed by constant\n" ^ Display.string_of_thm thm);
+ | _ => bad_thm ("Equation not headed by constant\n" ^ Display.string_of_thm_global thy thm);
fun check _ (Abs _) = bad_thm
("Abstraction on left hand side of equation\n"
- ^ Display.string_of_thm thm)
+ ^ Display.string_of_thm_global thy thm)
| check 0 (Var _) = ()
| check _ (Var _) = bad_thm
("Variable with application on left hand side of equation\n"
- ^ Display.string_of_thm thm)
+ ^ Display.string_of_thm_global thy thm)
| check n (t1 $ t2) = (check (n+1) t1; check 0 t2)
| check n (Const (c_ty as (c, ty))) = if n = (length o fst o strip_type) ty
then if not proper orelse is_constr_pat (AxClass.unoverload_const thy c_ty)
then ()
else bad_thm (quote c ^ " is not a constructor, on left hand side of equation\n"
- ^ Display.string_of_thm thm)
+ ^ Display.string_of_thm_global thy thm)
else bad_thm
("Partially applied constant " ^ quote c ^ " on left hand side of equation\n"
- ^ Display.string_of_thm thm);
+ ^ Display.string_of_thm_global thy thm);
val _ = map (check 0) args;
val _ = if not proper orelse is_linear thm then ()
else bad_thm ("Duplicate variables on left hand side of equation\n"
- ^ Display.string_of_thm thm);
+ ^ Display.string_of_thm_global thy thm);
val _ = if (is_none o AxClass.class_of_param thy) c
then ()
else bad_thm ("Polymorphic constant as head in equation\n"
- ^ Display.string_of_thm thm)
+ ^ Display.string_of_thm_global thy thm)
val _ = if not (is_constr thy c)
then ()
else bad_thm ("Constructor as head in equation\n"
- ^ Display.string_of_thm thm)
+ ^ Display.string_of_thm_global thy thm)
val ty_decl = Sign.the_const_type thy c;
val _ = if Sign.typ_equiv thy (Type.strip_sorts ty_decl, Type.strip_sorts ty)
then () else bad_thm ("Type\n" ^ string_of_typ thy ty
^ "\nof equation\n"
- ^ Display.string_of_thm thm
+ ^ Display.string_of_thm_global thy thm
^ "\nis incompatible with declared function type\n"
^ string_of_typ thy ty_decl)
in (thm, proper) end;
@@ -657,7 +659,7 @@
let
fun cert (eqn as (thm, _)) = if c = const_eqn thy thm
then eqn else error ("Wrong head of code equation,\nexpected constant "
- ^ string_of_const thy c ^ "\n" ^ Display.string_of_thm thm)
+ ^ string_of_const thy c ^ "\n" ^ Display.string_of_thm_global thy thm)
in map (cert o assert_eqn thy) eqns end;
fun common_typ_eqns thy [] = []
@@ -674,7 +676,7 @@
fun unify ty env = Sign.typ_unify thy (ty1, ty) env
handle Type.TUNIFY =>
error ("Type unificaton failed, while unifying code equations\n"
- ^ (cat_lines o map Display.string_of_thm) thms
+ ^ (cat_lines o map (Display.string_of_thm_global thy)) thms
^ "\nwith types\n"
^ (cat_lines o map (string_of_typ thy)) (ty1 :: tys));
val (env, _) = fold unify tys (Vartab.empty, maxidx)
@@ -796,15 +798,15 @@
let
val (ofclass, eqn) = case try Logic.dest_equals (Thm.prop_of thm)
of SOME ofclass_eq => ofclass_eq
- | _ => error ("Bad certificate: " ^ Display.string_of_thm thm);
+ | _ => error ("Bad certificate: " ^ Display.string_of_thm_global thy thm);
val (T, class) = case try Logic.dest_of_class ofclass
of SOME T_class => T_class
- | _ => error ("Bad certificate: " ^ Display.string_of_thm thm);
+ | _ => error ("Bad certificate: " ^ Display.string_of_thm_global thy thm);
val tvar = case try Term.dest_TVar T
of SOME tvar => tvar
- | _ => error ("Bad type: " ^ Display.string_of_thm thm);
+ | _ => error ("Bad type: " ^ Display.string_of_thm_global thy thm);
val _ = if Term.add_tvars eqn [] = [tvar] then ()
- else error ("Inconsistent type: " ^ Display.string_of_thm thm);
+ else error ("Inconsistent type: " ^ Display.string_of_thm_global thy thm);
val lhs_rhs = case try Logic.dest_equals eqn
of SOME lhs_rhs => lhs_rhs
| _ => error ("Not an equation: " ^ Syntax.string_of_term_global thy eqn);
@@ -813,7 +815,7 @@
| _ => error ("Not an equation with two constants: "
^ Syntax.string_of_term_global thy eqn);
val _ = if the_list (AxClass.class_of_param thy (snd c_c')) = [class] then ()
- else error ("Inconsistent class: " ^ Display.string_of_thm thm);
+ else error ("Inconsistent class: " ^ Display.string_of_thm_global thy thm);
in thy |>
(map_exec_purge NONE o map_aliasses) (fn (alias, classes) =>
((c_c', thm) :: alias, insert (op =) class classes))
--- a/src/Pure/Isar/context_rules.ML Tue Jul 21 00:56:19 2009 +0200
+++ b/src/Pure/Isar/context_rules.ML Tue Jul 21 01:03:18 2009 +0200
@@ -116,7 +116,7 @@
fun prt_kind (i, b) =
Pretty.big_list ((the o AList.lookup (op =) kind_names) (i, b) ^ ":")
(map_filter (fn (_, (k, th)) =>
- if k = (i, b) then SOME (ProofContext.pretty_thm ctxt th) else NONE)
+ if k = (i, b) then SOME (Display.pretty_thm ctxt th) else NONE)
(sort (int_ord o pairself fst) rules));
in Pretty.writeln (Pretty.chunks (map prt_kind rule_kinds)) end;
--- a/src/Pure/Isar/element.ML Tue Jul 21 00:56:19 2009 +0200
+++ b/src/Pure/Isar/element.ML Tue Jul 21 01:03:18 2009 +0200
@@ -163,7 +163,7 @@
let
val prt_typ = Pretty.quote o Syntax.pretty_typ ctxt;
val prt_term = Pretty.quote o Syntax.pretty_term ctxt;
- val prt_thm = Pretty.backquote o ProofContext.pretty_thm ctxt;
+ val prt_thm = Pretty.backquote o Display.pretty_thm ctxt;
val prt_name_atts = pretty_name_atts ctxt;
fun prt_mixfix NoSyn = []
--- a/src/Pure/Isar/isar_cmd.ML Tue Jul 21 00:56:19 2009 +0200
+++ b/src/Pure/Isar/isar_cmd.ML Tue Jul 21 01:03:18 2009 +0200
@@ -442,8 +442,7 @@
|> Pretty.chunks2 |> Pretty.string_of;
fun string_of_thms state args =
- Pretty.string_of (ProofContext.pretty_thms (Proof.context_of state)
- (Proof.get_thmss state args));
+ Pretty.string_of (Display.pretty_thms (Proof.context_of state) (Proof.get_thmss state args));
fun string_of_prfs full state arg =
Pretty.string_of (case arg of
--- a/src/Pure/Isar/local_defs.ML Tue Jul 21 00:56:19 2009 +0200
+++ b/src/Pure/Isar/local_defs.ML Tue Jul 21 01:03:18 2009 +0200
@@ -196,7 +196,7 @@
fun print_rules ctxt =
Pretty.writeln (Pretty.big_list "definitional transformations:"
- (map (ProofContext.pretty_thm ctxt) (Rules.get (Context.Proof ctxt))));
+ (map (Display.pretty_thm ctxt) (Rules.get (Context.Proof ctxt))));
val defn_add = Thm.declaration_attribute (Rules.map o Thm.add_thm);
val defn_del = Thm.declaration_attribute (Rules.map o Thm.del_thm);
--- a/src/Pure/Isar/method.ML Tue Jul 21 00:56:19 2009 +0200
+++ b/src/Pure/Isar/method.ML Tue Jul 21 01:03:18 2009 +0200
@@ -220,7 +220,7 @@
fun trace ctxt rules =
if ! trace_rules andalso not (null rules) then
- Pretty.big_list "rules:" (map (ProofContext.pretty_thm ctxt) rules)
+ Pretty.big_list "rules:" (map (Display.pretty_thm ctxt) rules)
|> Pretty.string_of |> tracing
else ();
--- a/src/Pure/Isar/obtain.ML Tue Jul 21 00:56:19 2009 +0200
+++ b/src/Pure/Isar/obtain.ML Tue Jul 21 01:03:18 2009 +0200
@@ -180,9 +180,9 @@
[prem] =>
if Thm.concl_of th aconv thesis andalso
Logic.strip_assums_concl prem aconv thesis then th
- else error ("Guessed a different clause:\n" ^ ProofContext.string_of_thm ctxt th)
+ else error ("Guessed a different clause:\n" ^ Display.string_of_thm ctxt th)
| [] => error "Goal solved -- nothing guessed."
- | _ => error ("Guess split into several cases:\n" ^ ProofContext.string_of_thm ctxt th));
+ | _ => error ("Guess split into several cases:\n" ^ Display.string_of_thm ctxt th));
fun result tac facts ctxt =
let
@@ -218,7 +218,7 @@
val string_of_typ = Syntax.string_of_typ ctxt;
val string_of_term = setmp show_types true (Syntax.string_of_term ctxt);
- fun err msg th = error (msg ^ ":\n" ^ ProofContext.string_of_thm ctxt th);
+ fun err msg th = error (msg ^ ":\n" ^ Display.string_of_thm ctxt th);
val maxidx = fold (Term.maxidx_typ o snd o fst) vars ~1;
val rule = Thm.incr_indexes (maxidx + 1) raw_rule;
--- a/src/Pure/Isar/proof.ML Tue Jul 21 00:56:19 2009 +0200
+++ b/src/Pure/Isar/proof.ML Tue Jul 21 01:03:18 2009 +0200
@@ -322,7 +322,7 @@
fun pretty_facts _ _ NONE = []
| pretty_facts s ctxt (SOME ths) =
- [Pretty.big_list (s ^ "this:") (map (ProofContext.pretty_thm ctxt) ths), Pretty.str ""];
+ [Pretty.big_list (s ^ "this:") (map (Display.pretty_thm ctxt) ths), Pretty.str ""];
fun pretty_state nr state =
let
@@ -470,7 +470,7 @@
let
val thy = ProofContext.theory_of ctxt;
val string_of_term = Syntax.string_of_term ctxt;
- val string_of_thm = ProofContext.string_of_thm ctxt;
+ val string_of_thm = Display.string_of_thm ctxt;
val ngoals = Thm.nprems_of goal;
val _ = ngoals = 0 orelse error (Pretty.string_of (Pretty.chunks
--- a/src/Pure/Isar/proof_display.ML Tue Jul 21 00:56:19 2009 +0200
+++ b/src/Pure/Isar/proof_display.ML Tue Jul 21 01:03:18 2009 +0200
@@ -35,7 +35,7 @@
let
val thy = Thm.theory_of_thm th;
val flags = {quote = true, show_hyps = false, show_status = true};
- in Display.pretty_thm_aux (Syntax.pp_global thy) flags [] th end;
+ in Display.pretty_thm_raw (Syntax.pp_global thy) flags [] th end;
val pp_typ = Pretty.quote oo Syntax.pretty_typ_global;
val pp_term = Pretty.quote oo Syntax.pretty_term_global;
@@ -68,7 +68,7 @@
fun pretty_rule ctxt s thm =
Pretty.block [Pretty.str (s ^ " attempt to solve goal by exported rule:"),
- Pretty.fbrk, ProofContext.pretty_thm_aux ctxt false thm];
+ Pretty.fbrk, Display.pretty_thm_aux ctxt false thm];
val string_of_rule = Pretty.string_of ooo pretty_rule;
--- a/src/Pure/Isar/runtime.ML Tue Jul 21 00:56:19 2009 +0200
+++ b/src/Pure/Isar/runtime.ML Tue Jul 21 01:03:18 2009 +0200
@@ -75,7 +75,7 @@
| exn_msg ctxt (exn as TERM (msg, ts)) = raised exn "TERM" (msg ::
(if detailed then if_context ctxt Syntax.string_of_term ts else []))
| exn_msg ctxt (exn as THM (msg, i, thms)) = raised exn ("THM " ^ string_of_int i) (msg ::
- (if detailed then if_context ctxt ProofContext.string_of_thm thms else []))
+ (if detailed then if_context ctxt Display.string_of_thm thms else []))
| exn_msg _ exn = raised exn (General.exnMessage exn) [];
in exn_msg NONE e end;
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML Tue Jul 21 00:56:19 2009 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Tue Jul 21 01:03:18 2009 +0200
@@ -655,7 +655,7 @@
text=[XML.Elem("pgml",[],
maps YXML.parse_body strings)] })
- fun string_of_thm th = Pretty.string_of (Display.pretty_thm_aux
+ fun string_of_thm th = Pretty.string_of (Display.pretty_thm_raw
(Syntax.pp_global (Thm.theory_of_thm th))
{quote = false, show_hyps = false, show_status = true} [] th)
--- a/src/Pure/Tools/find_theorems.ML Tue Jul 21 00:56:19 2009 +0200
+++ b/src/Pure/Tools/find_theorems.ML Tue Jul 21 01:03:18 2009 +0200
@@ -408,7 +408,7 @@
fun pretty_thm ctxt (thmref, thm) = Pretty.block
[Pretty.str (Facts.string_of_ref thmref), Pretty.str ":", Pretty.brk 1,
- ProofContext.pretty_thm ctxt thm];
+ Display.pretty_thm ctxt thm];
fun print_theorems ctxt opt_goal opt_limit rem_dups raw_criteria =
let
--- a/src/Pure/old_goals.ML Tue Jul 21 00:56:19 2009 +0200
+++ b/src/Pure/old_goals.ML Tue Jul 21 01:03:18 2009 +0200
@@ -199,7 +199,7 @@
case e of
THM (msg,i,thms) =>
(writeln ("Exception THM " ^ string_of_int i ^ " raised:\n" ^ msg);
- List.app Display.print_thm thms)
+ List.app (writeln o Display.string_of_thm_global thy) thms)
| THEORY (msg,thys) =>
(writeln ("Exception THEORY raised:\n" ^ msg);
List.app (writeln o Context.str_of_thy) thys)
--- a/src/Pure/simplifier.ML Tue Jul 21 00:56:19 2009 +0200
+++ b/src/Pure/simplifier.ML Tue Jul 21 01:03:18 2009 +0200
@@ -79,7 +79,7 @@
fun pretty_ss ctxt ss =
let
val pretty_cterm = Syntax.pretty_term ctxt o Thm.term_of;
- val pretty_thm = ProofContext.pretty_thm ctxt;
+ val pretty_thm = Display.pretty_thm ctxt;
fun pretty_proc (name, lhss) = Pretty.big_list (name ^ ":") (map pretty_cterm lhss);
fun pretty_cong (name, thm) =
Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 1, pretty_thm thm];
--- a/src/Sequents/prover.ML Tue Jul 21 00:56:19 2009 +0200
+++ b/src/Sequents/prover.ML Tue Jul 21 01:03:18 2009 +0200
@@ -27,7 +27,8 @@
fun warn_duplicates [] = []
| warn_duplicates dups =
- (warning (cat_lines ("Ignoring duplicate theorems:" :: map Display.string_of_thm dups));
+ (warning (cat_lines ("Ignoring duplicate theorems:" ::
+ map Display.string_of_thm_without_context dups));
dups);
fun (Pack(safes,unsafes)) add_safes ths =
@@ -50,8 +51,9 @@
fun print_pack (Pack(safes,unsafes)) =
- (writeln "Safe rules:"; Display.print_thms safes;
- writeln "Unsafe rules:"; Display.print_thms unsafes);
+ writeln (cat_lines
+ (["Safe rules:"] @ map Display.string_of_thm_without_context safes @
+ ["Unsafe rules:"] @ map Display.string_of_thm_without_context unsafes));
(*Returns the list of all formulas in the sequent*)
fun forms_of_seq (Const("SeqO'",_) $ P $ u) = P :: forms_of_seq u
--- a/src/Sequents/simpdata.ML Tue Jul 21 00:56:19 2009 +0200
+++ b/src/Sequents/simpdata.ML Tue Jul 21 01:03:18 2009 +0200
@@ -40,7 +40,7 @@
| (Const("Not",_)$_) => th RS @{thm iff_reflection_F}
| _ => th RS @{thm iff_reflection_T})
| _ => error ("addsimps: unable to use theorem\n" ^
- Display.string_of_thm th));
+ Display.string_of_thm_without_context th));
(*Replace premises x=y, X<->Y by X==Y*)
val mk_meta_prems =
--- a/src/Tools/Code/code_preproc.ML Tue Jul 21 00:56:19 2009 +0200
+++ b/src/Tools/Code/code_preproc.ML Tue Jul 21 01:03:18 2009 +0200
@@ -210,7 +210,7 @@
|> map (fn (s, thms) =>
(Pretty.block o Pretty.fbreaks) (
Pretty.str s
- :: map (Display.pretty_thm o fst) thms
+ :: map (Display.pretty_thm_global thy o fst) thms
))
|> Pretty.chunks;
@@ -523,7 +523,7 @@
in
Thm.transitive thm1 (Thm.transitive thm2 thm3) handle THM _ =>
error ("could not construct evaluation proof:\n"
- ^ (cat_lines o map Display.string_of_thm) [thm1, thm2, thm3])
+ ^ (cat_lines o map (Display.string_of_thm_global thy)) [thm1, thm2, thm3])
end;
in gen_eval thy I conclude_evaluation end;
--- a/src/Tools/Code/code_printer.ML Tue Jul 21 00:56:19 2009 +0200
+++ b/src/Tools/Code/code_printer.ML Tue Jul 21 01:03:18 2009 +0200
@@ -82,7 +82,7 @@
open Code_Thingol;
-fun nerror thm s = error (s ^ ",\nin equation " ^ Display.string_of_thm thm);
+fun nerror thm s = error (s ^ ",\nin equation " ^ Display.string_of_thm_without_context thm);
(** assembling text pieces **)
--- a/src/Tools/Code/code_thingol.ML Tue Jul 21 00:56:19 2009 +0200
+++ b/src/Tools/Code/code_thingol.ML Tue Jul 21 01:03:18 2009 +0200
@@ -469,7 +469,7 @@
let
val err_class = Sorts.class_error (Syntax.pp_global thy) e;
val err_thm = case thm
- of SOME thm => "\n(in code equation " ^ Display.string_of_thm thm ^ ")" | NONE => "";
+ of SOME thm => "\n(in code equation " ^ Display.string_of_thm_global thy thm ^ ")" | NONE => "";
val err_typ = "Type " ^ Syntax.string_of_typ_global thy ty ^ " not of sort "
^ Syntax.string_of_sort_global thy sort;
in error ("Wellsortedness error" ^ err_thm ^ ":\n" ^ err_typ ^ "\n" ^ err_class) end;
--- a/src/Tools/coherent.ML Tue Jul 21 00:56:19 2009 +0200
+++ b/src/Tools/coherent.ML Tue Jul 21 01:03:18 2009 +0200
@@ -177,7 +177,7 @@
fun thm_of_cl_prf thy goal asms (ClPrf (th, (tye, env), insts, is, prfs)) =
let
val _ = message (fn () => space_implode "\n"
- ("asms:" :: map Display.string_of_thm asms) ^ "\n\n");
+ ("asms:" :: map (Display.string_of_thm_global thy) asms) ^ "\n\n");
val th' = Drule.implies_elim_list
(Thm.instantiate
(map (fn (ixn, (S, T)) =>
--- a/src/Tools/induct.ML Tue Jul 21 00:56:19 2009 +0200
+++ b/src/Tools/induct.ML Tue Jul 21 01:03:18 2009 +0200
@@ -124,7 +124,7 @@
fun pretty_rules ctxt kind rs =
let val thms = map snd (Item_Net.content rs)
- in Pretty.big_list kind (map (ProofContext.pretty_thm ctxt) thms) end;
+ in Pretty.big_list kind (map (Display.pretty_thm ctxt) thms) end;
(* context data *)
--- a/src/ZF/Tools/inductive_package.ML Tue Jul 21 00:56:19 2009 +0200
+++ b/src/ZF/Tools/inductive_package.ML Tue Jul 21 01:03:18 2009 +0200
@@ -247,8 +247,7 @@
(intr_tms, map intro_tacsf (mk_disj_rls (length intr_tms)))
|> ListPair.map (fn (t, tacs) =>
Goal.prove_global thy1 [] [] t
- (fn _ => EVERY (rewrite_goals_tac part_rec_defs :: tacs)))
- handle MetaSimplifier.SIMPLIFIER (msg, thm) => (Display.print_thm thm; error msg);
+ (fn _ => EVERY (rewrite_goals_tac part_rec_defs :: tacs)));
(********)
val dummy = writeln " Proving the elimination rule...";
@@ -318,11 +317,12 @@
val ind_prems = map (induct_prem (map (rpair pred) rec_tms))
intr_tms;
- val dummy = if !Ind_Syntax.trace then
- (writeln "ind_prems = ";
- List.app (writeln o Syntax.string_of_term ctxt1) ind_prems;
- writeln "raw_induct = "; Display.print_thm raw_induct)
- else ();
+ val dummy =
+ if ! Ind_Syntax.trace then
+ writeln (cat_lines
+ (["ind_prems:"] @ map (Syntax.string_of_term ctxt1) ind_prems @
+ ["raw_induct:", Display.string_of_thm ctxt1 raw_induct]))
+ else ();
(*We use a MINIMAL simpset. Even FOL_ss contains too many simpules.
@@ -351,9 +351,10 @@
ORELSE' bound_hyp_subst_tac)),
ind_tac (rev (map (rewrite_rule part_rec_defs) prems)) (length prems)]);
- val dummy = if !Ind_Syntax.trace then
- (writeln "quant_induct = "; Display.print_thm quant_induct)
- else ();
+ val dummy =
+ if ! Ind_Syntax.trace then
+ writeln ("quant_induct:\n" ^ Display.string_of_thm ctxt1 quant_induct)
+ else ();
(*** Prove the simultaneous induction rule ***)
@@ -426,9 +427,10 @@
REPEAT (rewrite_goals_tac [Pr.split_eq] THEN lemma_tac 1)]))
else (writeln " [ No mutual induction rule needed ]"; @{thm TrueI});
- val dummy = if !Ind_Syntax.trace then
- (writeln "lemma = "; Display.print_thm lemma)
- else ();
+ val dummy =
+ if ! Ind_Syntax.trace then
+ writeln ("lemma: " ^ Display.string_of_thm ctxt1 lemma)
+ else ();
(*Mutual induction follows by freeness of Inl/Inr.*)
--- a/src/ZF/Tools/typechk.ML Tue Jul 21 00:56:19 2009 +0200
+++ b/src/ZF/Tools/typechk.ML Tue Jul 21 01:03:18 2009 +0200
@@ -27,7 +27,8 @@
fun add_rule th (tcs as TC {rules, net}) =
if member Thm.eq_thm_prop rules th then
- (warning ("Ignoring duplicate type-checking rule\n" ^ Display.string_of_thm th); tcs)
+ (warning ("Ignoring duplicate type-checking rule\n" ^
+ Display.string_of_thm_without_context th); tcs)
else
TC {rules = th :: rules,
net = Net.insert_term (K false) (Thm.concl_of th, th) net};
@@ -36,7 +37,8 @@
if member Thm.eq_thm_prop rules th then
TC {net = Net.delete_term Thm.eq_thm_prop (Thm.concl_of th, th) net,
rules = remove Thm.eq_thm_prop th rules}
- else (warning ("No such type-checking rule\n" ^ Display.string_of_thm th); tcs);
+ else (warning ("No such type-checking rule\n" ^
+ Display.string_of_thm_without_context th); tcs);
(* generic data *)
@@ -60,7 +62,7 @@
fun print_tcset ctxt =
let val TC {rules, ...} = tcset_of ctxt in
Pretty.writeln (Pretty.big_list "type-checking rules:"
- (map (ProofContext.pretty_thm ctxt) rules))
+ (map (Display.pretty_thm ctxt) rules))
end;