--- a/NEWS Fri Sep 25 20:04:25 2015 +0200
+++ b/NEWS Fri Sep 25 20:37:59 2015 +0200
@@ -328,6 +328,10 @@
*** ML ***
+* The auxiliary module Pure/display.ML has been eliminated. Its
+elementary thm print operations are now in Pure/more_thm.ML and thus
+called Thm.pretty_thm, Thm.string_of_thm etc. INCOMPATIBILITY.
+
* Simproc programming interfaces have been simplified:
Simplifier.make_simproc and Simplifier.define_simproc supersede various
forms of Simplifier.mk_simproc, Simplifier.simproc_global etc. Note that
--- a/src/FOL/ex/Locale_Test/Locale_Test1.thy Fri Sep 25 20:04:25 2015 +0200
+++ b/src/FOL/ex/Locale_Test/Locale_Test1.thy Fri Sep 25 20:37:59 2015 +0200
@@ -151,7 +151,7 @@
fun check_syntax ctxt thm expected =
let
val obtained =
- Print_Mode.setmp [] (Display.string_of_thm (Config.put show_markup false ctxt)) thm;
+ Print_Mode.setmp [] (Thm.string_of_thm (Config.put show_markup false ctxt)) thm;
in
if obtained <> expected
then error ("Theorem syntax '" ^ obtained ^ "' obtained, but '" ^ expected ^ "' expected.")
--- a/src/FOLP/classical.ML Fri Sep 25 20:04:25 2015 +0200
+++ b/src/FOLP/classical.ML Fri Sep 25 20:37:59 2015 +0200
@@ -124,10 +124,10 @@
fun print_cs ctxt (CS{safeIs,safeEs,hazIs,hazEs,...}) =
writeln (cat_lines
- (["Introduction rules"] @ map (Display.string_of_thm ctxt) hazIs @
- ["Safe introduction rules"] @ map (Display.string_of_thm ctxt) safeIs @
- ["Elimination rules"] @ map (Display.string_of_thm ctxt) hazEs @
- ["Safe elimination rules"] @ map (Display.string_of_thm ctxt) safeEs));
+ (["Introduction rules"] @ map (Thm.string_of_thm ctxt) hazIs @
+ ["Safe introduction rules"] @ map (Thm.string_of_thm ctxt) safeIs @
+ ["Elimination rules"] @ map (Thm.string_of_thm ctxt) hazEs @
+ ["Safe elimination rules"] @ map (Thm.string_of_thm ctxt) safeEs));
fun (CS{safeIs,safeEs,hazIs,hazEs,...}) addSIs ths =
make_cs {safeIs=ths@safeIs, safeEs=safeEs, hazIs=hazIs, hazEs=hazEs};
--- a/src/FOLP/simp.ML Fri Sep 25 20:04:25 2015 +0200
+++ b/src/FOLP/simp.ML Fri Sep 25 20:37:59 2015 +0200
@@ -306,8 +306,8 @@
fun print_ss ctxt (SS{congs,simps,...}) =
writeln (cat_lines
- (["Congruences:"] @ map (Display.string_of_thm ctxt) congs @
- ["Rewrite Rules:"] @ map (Display.string_of_thm ctxt o #1) simps));
+ (["Congruences:"] @ map (Thm.string_of_thm ctxt) congs @
+ ["Rewrite Rules:"] @ map (Thm.string_of_thm ctxt o #1) simps));
(* Rewriting with conditionals *)
--- a/src/HOL/Eisbach/Eisbach_Tools.thy Fri Sep 25 20:04:25 2015 +0200
+++ b/src/HOL/Eisbach/Eisbach_Tools.thy Fri Sep 25 20:37:59 2015 +0200
@@ -31,7 +31,7 @@
(Scan.lift (Scan.ahead Parse.not_eof) -- Attrib.thms)
(fn ctxt => fn (tok, thms) =>
(* FIXME proper formatting!? *)
- Token.unparse tok ^ ": " ^ commas (map (Display.string_of_thm ctxt) thms)) #>
+ Token.unparse tok ^ ": " ^ commas (map (Thm.string_of_thm ctxt) thms)) #>
setup_trace_method @{binding print_term}
(Scan.lift (Scan.ahead Parse.not_eof) -- Args.term)
(fn ctxt => fn (tok, t) =>
--- a/src/HOL/Library/Old_SMT/old_smt_normalize.ML Fri Sep 25 20:04:25 2015 +0200
+++ b/src/HOL/Library/Old_SMT/old_smt_normalize.ML Fri Sep 25 20:37:59 2015 +0200
@@ -21,7 +21,7 @@
fun drop_fact_warning ctxt =
Old_SMT_Config.verbose_msg ctxt (prefix "Warning: dropping assumption: " o
- Display.string_of_thm ctxt)
+ Thm.string_of_thm ctxt)
(* general theorem normalizations *)
--- a/src/HOL/Library/Old_SMT/old_smt_solver.ML Fri Sep 25 20:04:25 2015 +0200
+++ b/src/HOL/Library/Old_SMT/old_smt_solver.ML Fri Sep 25 20:37:59 2015 +0200
@@ -105,7 +105,7 @@
fun trace_assms ctxt =
Old_SMT_Config.trace_msg ctxt (Pretty.string_of o
- Pretty.big_list "Assertions:" o map (Display.pretty_thm ctxt o snd))
+ Pretty.big_list "Assertions:" o map (Thm.pretty_thm ctxt o snd))
fun trace_recon_data ({context=ctxt, typs, terms, ...} : Old_SMT_Translate.recon) =
let
@@ -327,7 +327,7 @@
if Config.get ctxt Old_SMT_Config.trace_used_facts andalso length wthms > 0
then
tracing (Pretty.string_of (Pretty.big_list "SMT used facts:"
- (map (Display.pretty_thm ctxt o snd) wthms)))
+ (map (Thm.pretty_thm ctxt o snd) wthms)))
else ()
end
--- a/src/HOL/Library/Old_SMT/old_z3_proof_reconstruction.ML Fri Sep 25 20:04:25 2015 +0200
+++ b/src/HOL/Library/Old_SMT/old_z3_proof_reconstruction.ML Fri Sep 25 20:37:59 2015 +0200
@@ -72,7 +72,7 @@
fun pretty_goal ctxt thms t =
[Pretty.block [Pretty.str "proposition: ", Syntax.pretty_term ctxt t]]
|> not (null thms) ? cons (Pretty.big_list "assumptions:"
- (map (Display.pretty_thm ctxt) thms))
+ (map (Thm.pretty_thm ctxt) thms))
fun try_apply ctxt thms =
let
--- a/src/HOL/Library/old_recdef.ML Fri Sep 25 20:04:25 2015 +0200
+++ b/src/HOL/Library/old_recdef.ML Fri Sep 25 20:37:59 2015 +0200
@@ -375,8 +375,8 @@
(case find_thms_split splitths 1 th of
NONE =>
(writeln (cat_lines
- (["th:", Display.string_of_thm ctxt th, "split ths:"] @
- map (Display.string_of_thm ctxt) splitths @ ["\n--"]));
+ (["th:", Thm.string_of_thm ctxt th, "split ths:"] @
+ map (Thm.string_of_thm ctxt) splitths @ ["\n--"]));
error "splitto: cannot find variable to split on")
| SOME v =>
let
@@ -1342,7 +1342,7 @@
fun say s = if !tracing then writeln s else ();
fun print_thms ctxt s L =
- say (cat_lines (s :: map (Display.string_of_thm ctxt) L));
+ say (cat_lines (s :: map (Thm.string_of_thm ctxt) L));
fun print_term ctxt s t =
say (cat_lines [s, Syntax.string_of_term ctxt t]);
@@ -1458,7 +1458,7 @@
val cntxt = Simplifier.prems_of ctxt
val _ = print_thms ctxt "cntxt:" cntxt
val _ = say "cong rule:"
- val _ = say (Display.string_of_thm ctxt thm)
+ val _ = say (Thm.string_of_thm ctxt thm)
(* Unquantified eliminate *)
fun uq_eliminate (thm,imp) =
let val tych = Thm.cterm_of ctxt
@@ -2390,7 +2390,7 @@
fun trace_thms ctxt s L =
- if !trace then writeln (cat_lines (s :: map (Display.string_of_thm ctxt) L))
+ if !trace then writeln (cat_lines (s :: map (Thm.string_of_thm ctxt) L))
else ();
fun trace_cterm ctxt s ct =
--- a/src/HOL/Nominal/nominal_thmdecls.ML Fri Sep 25 20:04:25 2015 +0200
+++ b/src/HOL/Nominal/nominal_thmdecls.ML Fri Sep 25 20:37:59 2015 +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 (Context.proof_of context) orig_thm ^
+ error (Thm.string_of_thm (Context.proof_of context) orig_thm ^
" does not comply with the form of an equivariance lemma (" ^ s ^").")
--- a/src/HOL/SPARK/Tools/spark_commands.ML Fri Sep 25 20:04:25 2015 +0200
+++ b/src/HOL/SPARK/Tools/spark_commands.ML Fri Sep 25 20:37:59 2015 +0200
@@ -78,7 +78,7 @@
Pretty.chunks (map (fn (b, th) => Pretty.block
[Binding.pretty b, Pretty.str ":",
Pretty.brk 1,
- Display.pretty_thm ctxt th])
+ Thm.pretty_thm ctxt th])
defs),
Pretty.str "Verification conditions:",
--- a/src/HOL/Tools/Lifting/lifting_setup.ML Fri Sep 25 20:04:25 2015 +0200
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML Fri Sep 25 20:37:59 2015 +0200
@@ -202,14 +202,14 @@
raise QUOT_ERROR [Pretty.block
[Pretty.str "The Quotient theorem has extra assumptions:",
Pretty.brk 1,
- Display.pretty_thm ctxt quot_thm]]
+ Thm.pretty_thm ctxt quot_thm]]
else ()
val _ = quot_thm |> Thm.concl_of |> HOLogic.dest_Trueprop |> dest_Quotient
handle TERM _ => raise QUOT_ERROR
[Pretty.block
[Pretty.str "The Quotient theorem is not of the right form:",
Pretty.brk 1,
- Display.pretty_thm ctxt quot_thm]]
+ Thm.pretty_thm ctxt quot_thm]]
val ((_, [quot_thm_fixed]), ctxt') = Variable.importT [quot_thm] ctxt
val (rty, qty) = quot_thm_rty_qty quot_thm_fixed
val rty_tfreesT = Term.add_tfree_namesT rty []
@@ -837,13 +837,13 @@
handle TERM _ => raise PCR_ERROR [Pretty.block
[Pretty.str "The pcr definiton theorem is not a plain meta equation:",
Pretty.brk 1,
- Display.pretty_thm ctxt pcrel_def]]
+ Thm.pretty_thm ctxt pcrel_def]]
val pcr_const_def = head_of def_lhs
val (eq_lhs, eq_rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.prop_of pcr_cr_eq))
handle TERM _ => raise PCR_ERROR [Pretty.block
[Pretty.str "The pcr_cr equation theorem is not a plain equation:",
Pretty.brk 1,
- Display.pretty_thm ctxt pcr_cr_eq]]
+ Thm.pretty_thm ctxt pcr_cr_eq]]
val (pcr_const_eq, eqs) = strip_comb eq_lhs
fun is_eq (Const (@{const_name HOL.eq}, _)) = true
| is_eq _ = false
@@ -853,7 +853,7 @@
[Pretty.block
[Pretty.str "Arguments of the lhs of the pcr_cr equation theorem are not only equalities:",
Pretty.brk 1,
- Display.pretty_thm ctxt pcr_cr_eq]]
+ Thm.pretty_thm ctxt pcr_cr_eq]]
else []
val pcr_consts_not_equal = if not (eq_Const pcr_const_def pcr_const_eq) then
[Pretty.block
--- a/src/HOL/Tools/Meson/meson.ML Fri Sep 25 20:04:25 2015 +0200
+++ b/src/HOL/Tools/Meson/meson.ML Fri Sep 25 20:37:59 2015 +0200
@@ -186,8 +186,8 @@
| tacf prems =
error (cat_lines
("Bad proof state in forward_res, please inform lcp@cl.cam.ac.uk:" ::
- Display.string_of_thm ctxt st ::
- "Premises:" :: map (Display.string_of_thm ctxt) prems))
+ Thm.string_of_thm ctxt st ::
+ "Premises:" :: map (Thm.string_of_thm ctxt) prems))
in
case Seq.pull (ALLGOALS (Misc_Legacy.METAHYPS ctxt tacf) st) of
SOME (th, _) => th
@@ -395,7 +395,7 @@
val cls =
if has_too_many_clauses ctxt (Thm.concl_of th) then
(trace_msg ctxt (fn () =>
- "cnf is ignoring: " ^ Display.string_of_thm ctxt th); ths)
+ "cnf is ignoring: " ^ Thm.string_of_thm ctxt th); ths)
else
cnf_aux (th, ths)
in (cls, !ctxt_ref) end
@@ -652,7 +652,7 @@
|> tap (fn NONE =>
trace_msg ctxt (fn () =>
"Failed to skolemize " ^
- Display.string_of_thm ctxt th)
+ Thm.string_of_thm ctxt th)
| _ => ()))
end
@@ -751,8 +751,8 @@
val horns = make_horns (cls @ ths)
val _ = trace_msg ctxt (fn () =>
cat_lines ("meson method called:" ::
- map (Display.string_of_thm ctxt) (cls @ ths) @
- ["clauses:"] @ map (Display.string_of_thm ctxt) horns))
+ map (Thm.string_of_thm ctxt) (cls @ ths) @
+ ["clauses:"] @ map (Thm.string_of_thm ctxt) horns))
in
THEN_ITER_DEEPEN iter_deepen_limit
(resolve_tac ctxt goes 1) (has_fewer_prems 1) (prolog_step_tac' ctxt horns)
--- a/src/HOL/Tools/Meson/meson_clausify.ML Fri Sep 25 20:04:25 2015 +0200
+++ b/src/HOL/Tools/Meson/meson_clausify.ML Fri Sep 25 20:37:59 2015 +0200
@@ -170,7 +170,7 @@
val eqth = introduce_combinators_in_cterm ctxt (Thm.cprop_of th)
in Thm.equal_elim eqth th end
handle THM (msg, _, _) =>
- (warning ("Error in the combinator translation of " ^ Display.string_of_thm ctxt th ^
+ (warning ("Error in the combinator translation of " ^ Thm.string_of_thm ctxt th ^
"\nException message: " ^ msg);
(* A type variable of sort "{}" will make "abstraction" fail. *)
TrueI)
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML Fri Sep 25 20:04:25 2015 +0200
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Fri Sep 25 20:37:59 2015 +0200
@@ -134,11 +134,11 @@
end
handle Option.Option =>
(trace_msg ctxt (fn () =>
- "\"find_var\" failed for " ^ x ^ " in " ^ Display.string_of_thm ctxt i_th);
+ "\"find_var\" failed for " ^ x ^ " in " ^ Thm.string_of_thm ctxt i_th);
NONE)
| TYPE _ =>
(trace_msg ctxt (fn () =>
- "\"hol_term_of_metis\" failed for " ^ x ^ " in " ^ Display.string_of_thm ctxt i_th);
+ "\"hol_term_of_metis\" failed for " ^ x ^ " in " ^ Thm.string_of_thm ctxt i_th);
NONE)
fun remove_typeinst (a, t) =
let val a = Metis_Name.toString a in
@@ -149,7 +149,7 @@
SOME _ => NONE (* type instantiations are forbidden *)
| NONE => SOME (a, t) (* internal Metis var? *)))
end
- val _ = trace_msg ctxt (fn () => " isa th: " ^ Display.string_of_thm ctxt i_th)
+ val _ = trace_msg ctxt (fn () => " isa th: " ^ Thm.string_of_thm ctxt i_th)
val substs = map_filter remove_typeinst (Metis_Subst.toList fsubst)
val (vars, tms) =
ListPair.unzip (map_filter subst_translation substs)
@@ -269,8 +269,8 @@
let
val (i_th1, i_th2) = apply2 (lookth th_pairs) (th1, th2)
val _ = trace_msg ctxt (fn () =>
- " isa th1 (pos): " ^ Display.string_of_thm ctxt i_th1 ^ "\n\
- \ isa th2 (neg): " ^ Display.string_of_thm ctxt i_th2)
+ " isa th1 (pos): " ^ Thm.string_of_thm ctxt i_th1 ^ "\n\
+ \ isa th2 (neg): " ^ Thm.string_of_thm ctxt i_th2)
in
(* Trivial cases where one operand is type info *)
if Thm.eq_thm (TrueI, i_th1) then
@@ -369,7 +369,7 @@
val _ = trace_msg ctxt (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' = Thm.incr_indexes (imax+1) (if pos then subst_em else ssubst_em)
- val _ = trace_msg ctxt (fn () => "subst' " ^ Display.string_of_thm ctxt subst')
+ val _ = trace_msg ctxt (fn () => "subst' " ^ Thm.string_of_thm ctxt subst')
val eq_terms =
map (apply2 (Thm.cterm_of ctxt))
(ListPair.zip (Misc_Legacy.term_vars (Thm.prop_of subst'), [tm_abs, tm_subst, i_tm]))
@@ -462,7 +462,7 @@
val th = one_step ctxt type_enc concealed sym_tab th_pairs (fol_th, inf)
|> flexflex_first_order ctxt
|> resynchronize ctxt fol_th
- val _ = trace_msg ctxt (fn () => "ISABELLE THM: " ^ Display.string_of_thm ctxt th)
+ val _ = trace_msg ctxt (fn () => "ISABELLE THM: " ^ Thm.string_of_thm ctxt th)
val _ = trace_msg ctxt (fn () => "=============================================")
in
(fol_th, th) :: th_pairs
--- a/src/HOL/Tools/Metis/metis_tactic.ML Fri Sep 25 20:04:25 2015 +0200
+++ b/src/HOL/Tools/Metis/metis_tactic.ML Fri Sep 25 20:37:59 2015 +0200
@@ -160,7 +160,7 @@
val dischargers = map (fst o snd) th_cls_pairs
val cls = cls |> map (Drule.eta_contraction_rule #> do_lams)
val _ = trace_msg ctxt (K "FOL_SOLVE: CONJECTURE CLAUSES")
- val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) cls
+ val _ = app (fn th => trace_msg ctxt (fn () => Thm.string_of_thm ctxt th)) cls
val _ = trace_msg ctxt (fn () => "type_enc = " ^ type_enc)
val type_enc = type_enc_of_string Strict type_enc
val (sym_tab, axioms, ord_info, concealed) =
@@ -172,7 +172,7 @@
| get_isa_thm _ (Isa_Raw ith) = ith
val axioms = axioms |> map (fn (mth, ith) => (mth, get_isa_thm mth ith))
val _ = trace_msg ctxt (K "ISABELLE CLAUSES")
- val _ = app (fn (_, ith) => trace_msg ctxt (fn () => Display.string_of_thm ctxt ith)) axioms
+ val _ = app (fn (_, ith) => trace_msg ctxt (fn () => Thm.string_of_thm ctxt ith)) axioms
val _ = trace_msg ctxt (K "METIS CLAUSES")
val _ = app (fn (mth, _) => trace_msg ctxt (fn () => Metis_Thm.toString mth)) axioms
val _ = trace_msg ctxt (K "START METIS PROVE PROCESS")
@@ -200,7 +200,7 @@
val result = fold (replay_one_inference ctxt' type_enc concealed sym_tab) proof axioms
val used = map_filter (used_axioms axioms) proof
val _ = trace_msg ctxt (K "METIS COMPLETED; clauses actually used:")
- val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) used
+ val _ = app (fn th => trace_msg ctxt (fn () => Thm.string_of_thm ctxt th)) used
val (used_th_cls_pairs, unused_th_cls_pairs) =
List.partition (have_common_thm ctxt used o snd o snd) th_cls_pairs
val unused_ths = maps (snd o snd) unused_th_cls_pairs
@@ -217,7 +217,7 @@
();
(case result of
(_, ith) :: _ =>
- (trace_msg ctxt (fn () => "Success: " ^ Display.string_of_thm ctxt ith);
+ (trace_msg ctxt (fn () => "Success: " ^ Thm.string_of_thm ctxt ith);
[discharge_skolem_premises ctxt dischargers ith])
| _ => (trace_msg ctxt (K "Metis: No result"); []))
end
@@ -251,7 +251,7 @@
val unused = Unsynchronized.ref []
val type_encs = if null type_encs0 then partial_type_encs else type_encs0
val _ = trace_msg ctxt (fn () =>
- "Metis called with theorems\n" ^ cat_lines (map (Display.string_of_thm ctxt) ths))
+ "Metis called with theorems\n" ^ cat_lines (map (Thm.string_of_thm ctxt) ths))
val type_encs = type_encs |> maps unalias_type_enc
val combs = (lam_trans = combsN)
fun tac clause = resolve_tac ctxt (FOL_SOLVE unused type_encs lam_trans ctxt clause ths) 1
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML Fri Sep 25 20:04:25 2015 +0200
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Fri Sep 25 20:37:59 2015 +0200
@@ -355,7 +355,7 @@
fun print_intros ctxt gr consts =
tracing (cat_lines (map (fn const =>
"Constant " ^ const ^ "has intros:\n" ^
- cat_lines (map (Display.string_of_thm ctxt) (Graph.get_node gr const))) consts))
+ cat_lines (map (Thm.string_of_thm ctxt) (Graph.get_node gr const))) consts))
(* translation of moded predicates *)
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Fri Sep 25 20:04:25 2015 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Fri Sep 25 20:37:59 2015 +0200
@@ -23,14 +23,14 @@
tracing (msg ^
(cat_lines (map
(fn (c, intros) => "Introduction rule(s) of " ^ c ^ ":\n" ^
- commas (map (Display.string_of_thm_global thy) intros)) intross)))
+ commas (map (Thm.string_of_thm_global thy) intros)) intross)))
else ()
fun print_specs options thy specs =
if show_intermediate_results options then
map (fn (c, thms) =>
"Constant " ^ c ^ " has specification:\n" ^
- (cat_lines (map (Display.string_of_thm_global thy) thms)) ^ "\n") specs
+ (cat_lines (map (Thm.string_of_thm_global thy) thms)) ^ "\n") specs
|> cat_lines |> tracing
else ()
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Fri Sep 25 20:04:25 2015 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Fri Sep 25 20:37:59 2015 +0200
@@ -1079,7 +1079,7 @@
error ("Type mismatch of predicate " ^ fst (dest_Const pred) ^
" (trying to match " ^ Syntax.string_of_typ ctxt' (fastype_of pred') ^
" and " ^ Syntax.string_of_typ ctxt' (fastype_of pred) ^ ")" ^
- " in " ^ Display.string_of_thm ctxt' th)
+ " in " ^ Thm.string_of_thm ctxt' th)
in map (fn (xi, (S, T)) => ((xi, S), T)) (Vartab.dest subst) end
fun instantiate_typ th =
let
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Fri Sep 25 20:04:25 2015 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Fri Sep 25 20:37:59 2015 +0200
@@ -130,11 +130,11 @@
let
val _ = writeln ("predicate: " ^ pred)
val _ = writeln ("introrules: ")
- val _ = fold (fn thm => fn _ => writeln (Display.string_of_thm ctxt thm))
+ val _ = fold (fn thm => fn _ => writeln (Thm.string_of_thm ctxt thm))
(rev (Core_Data.intros_of ctxt pred)) ()
in
if Core_Data.has_elim ctxt pred then
- writeln ("elimrule: " ^ Display.string_of_thm ctxt (Core_Data.the_elim_of ctxt pred))
+ writeln ("elimrule: " ^ Thm.string_of_thm ctxt (Core_Data.the_elim_of ctxt pred))
else
writeln ("no elimrule defined")
end
@@ -1295,7 +1295,7 @@
else
error ("Format of introduction rule is invalid: tuples must be expanded:"
^ (Syntax.string_of_term_global thy arg) ^ " in " ^
- (Display.string_of_thm_global thy intro))
+ (Thm.string_of_thm_global thy intro))
| _ => true
val prems = Logic.strip_imp_prems (prop_of intro)
fun check_prem (Prem t) = forall check_arg args
@@ -1387,7 +1387,7 @@
(*val _ = map (check_format_of_intro_rule thy) (maps (intros_of thy) prednames)*)
val _ =
if show_intermediate_results options then
- tracing (commas (map (Display.string_of_thm ctxt) (maps (Core_Data.intros_of ctxt) prednames)))
+ tracing (commas (map (Thm.string_of_thm ctxt) (maps (Core_Data.intros_of ctxt) prednames)))
else ()
val (preds, all_vs, param_vs, all_modes, clauses) =
prepare_intrs options ctxt prednames (maps (Core_Data.intros_of ctxt) prednames)
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Fri Sep 25 20:04:25 2015 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Fri Sep 25 20:37:59 2015 +0200
@@ -217,7 +217,7 @@
val _ =
if show_intermediate_results options then
tracing ("Specification for " ^ (Syntax.string_of_term_global thy t) ^ ":\n" ^
- commas (map (Display.string_of_thm_global thy) spec))
+ commas (map (Thm.string_of_thm_global thy) spec))
else ()
in
spec
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Fri Sep 25 20:04:25 2015 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Fri Sep 25 20:37:59 2015 +0200
@@ -310,7 +310,7 @@
fun rewrite_intro thy intro =
let
fun lookup_pred t = lookup thy (Fun_Pred.get thy) t
- (*val _ = tracing ("Rewriting intro " ^ Display.string_of_thm_global thy intro)*)
+ (*val _ = tracing ("Rewriting intro " ^ Thm.string_of_thm_global thy intro)*)
val intro_t = Logic.unvarify_global (Thm.prop_of intro)
val (prems, concl) = Logic.strip_horn intro_t
val frees = map fst (Term.add_frees intro_t [])
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Fri Sep 25 20:04:25 2015 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Fri Sep 25 20:37:59 2015 +0200
@@ -192,7 +192,7 @@
fun print_specs options thy msg ths =
if show_intermediate_results options then
- (tracing (msg); tracing (commas (map (Display.string_of_thm_global thy) ths)))
+ (tracing (msg); tracing (commas (map (Thm.string_of_thm_global thy) ths)))
else
()
@@ -209,7 +209,7 @@
map (rewrite_intros ctxt) specs
else
error ("unexpected specification for constant " ^ quote constname ^ ":\n"
- ^ commas (map (quote o Display.string_of_thm_global thy) specs))
+ ^ commas (map (quote o Thm.string_of_thm_global thy) specs))
val if_beta = @{lemma "(if c then x else y) z = (if c then x z else y z)" by simp}
val intros = map (rewrite_rule ctxt [if_beta RS @{thm eq_reflection}]) intros
val _ = print_specs options thy "normalized intros" intros
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML Fri Sep 25 20:04:25 2015 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML Fri Sep 25 20:37:59 2015 +0200
@@ -306,7 +306,7 @@
val (_, ts) = strip_comb t
in
trace_tac ctxt options ("Term " ^ (Syntax.string_of_term ctxt t) ^
- " splitting with rules \n" ^ Display.string_of_thm ctxt split_asm)
+ " splitting with rules \n" ^ Thm.string_of_thm ctxt split_asm)
THEN TRY (Splitter.split_asm_tac ctxt [split_asm] 1
THEN (trace_tac ctxt options "after splitting with split_asm rules")
(* THEN (Simplifier.asm_full_simp_tac (put_simpset HOL_basic_ss ctxt) 1)
--- a/src/HOL/Tools/SMT/smt_normalize.ML Fri Sep 25 20:04:25 2015 +0200
+++ b/src/HOL/Tools/SMT/smt_normalize.ML Fri Sep 25 20:37:59 2015 +0200
@@ -23,7 +23,7 @@
fun drop_fact_warning ctxt =
SMT_Config.verbose_msg ctxt (prefix "Warning: dropping assumption: " o
- Display.string_of_thm ctxt)
+ Thm.string_of_thm ctxt)
(* general theorem normalizations *)
--- a/src/HOL/Tools/SMT/smt_solver.ML Fri Sep 25 20:04:25 2015 +0200
+++ b/src/HOL/Tools/SMT/smt_solver.ML Fri Sep 25 20:37:59 2015 +0200
@@ -103,7 +103,7 @@
fun trace_assms ctxt =
SMT_Config.trace_msg ctxt (Pretty.string_of o
- Pretty.big_list "Assertions:" o map (Display.pretty_thm ctxt o snd))
+ Pretty.big_list "Assertions:" o map (Thm.pretty_thm ctxt o snd))
fun trace_replay_data ({context = ctxt, typs, terms, ...} : SMT_Translate.replay_data) =
let
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Fri Sep 25 20:04:25 2015 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Fri Sep 25 20:37:59 2015 +0200
@@ -89,7 +89,7 @@
val ctxt = ctxt |> Config.put show_markup true
val assms = op @ assmsp
val time = Pretty.str ("[" ^ string_of_play_outcome outcome ^ "]")
- val assms = Pretty.enum " and " "using " " shows " (map (Display.pretty_thm ctxt) assms)
+ val assms = Pretty.enum " and " "using " " shows " (map (Thm.pretty_thm ctxt) assms)
val concl = Syntax.pretty_term ctxt concl
in
tracing (Pretty.string_of (Pretty.blk (2, Pretty.breaks [time, assms, concl])))
--- a/src/HOL/Tools/choice_specification.ML Fri Sep 25 20:04:25 2015 +0200
+++ b/src/HOL/Tools/choice_specification.ML Fri Sep 25 20:37:59 2015 +0200
@@ -148,7 +148,7 @@
fun add_final (thm, thy) =
if name = ""
then (thm, thy)
- else (writeln (" " ^ name ^ ": " ^ Display.string_of_thm_global thy thm);
+ else (writeln (" " ^ name ^ ": " ^ Thm.string_of_thm_global thy thm);
Global_Theory.store_thm (Binding.name name, thm) thy)
in
swap args
--- a/src/HOL/Tools/inductive.ML Fri Sep 25 20:04:25 2015 +0200
+++ b/src/HOL/Tools/inductive.ML Fri Sep 25 20:37:59 2015 +0200
@@ -236,7 +236,7 @@
(Pretty.str "(co)inductives:" ::
map (Pretty.mark_str o #1)
(Name_Space.markup_entries verbose ctxt space (Symtab.dest infos)))),
- Pretty.big_list "monotonicity rules:" (map (Display.pretty_thm_item ctxt) monos)]
+ Pretty.big_list "monotonicity rules:" (map (Thm.pretty_thm_item ctxt) monos)]
end |> Pretty.writeln_chunks;
@@ -269,7 +269,7 @@
dest_less_concl (Seq.hd (REPEAT (FIRSTGOAL
(resolve_tac ctxt [@{thm le_funI}, @{thm le_boolI'}])) thm))
| _ => thm)
- end handle THM _ => error ("Bad monotonicity theorem:\n" ^ Display.string_of_thm ctxt thm);
+ end handle THM _ => error ("Bad monotonicity theorem:\n" ^ Thm.string_of_thm ctxt thm);
val mono_add =
Thm.declaration_attribute (fn thm => fn context =>
--- a/src/HOL/Tools/inductive_set.ML Fri Sep 25 20:04:25 2015 +0200
+++ b/src/HOL/Tools/inductive_set.ML Fri Sep 25 20:37:59 2015 +0200
@@ -298,7 +298,7 @@
val _ =
if Context_Position.is_really_visible ctxt then
warning ("Ignoring malformed set / predicate conversion rule: " ^ msg ^
- "\n" ^ Display.string_of_thm ctxt thm)
+ "\n" ^ Thm.string_of_thm ctxt thm)
else ();
in tab end;
--- a/src/HOL/Tools/lin_arith.ML Fri Sep 25 20:04:25 2015 +0200
+++ b/src/HOL/Tools/lin_arith.ML Fri Sep 25 20:37:59 2015 +0200
@@ -303,11 +303,11 @@
@{const_name Rings.divide}] a
| _ =>
(if Context_Position.is_visible ctxt then
- warning ("Lin. Arith.: wrong format for split rule " ^ Display.string_of_thm ctxt thm)
+ warning ("Lin. Arith.: wrong format for split rule " ^ Thm.string_of_thm ctxt thm)
else (); false))
| _ =>
(if Context_Position.is_visible ctxt then
- warning ("Lin. Arith.: wrong format for split rule " ^ Display.string_of_thm ctxt thm)
+ warning ("Lin. Arith.: wrong format for split rule " ^ Thm.string_of_thm ctxt thm)
else (); false));
(* substitute new for occurrences of old in a term, incrementing bound *)
--- a/src/HOL/Tools/sat.ML Fri Sep 25 20:04:25 2015 +0200
+++ b/src/HOL/Tools/sat.ML Fri Sep 25 20:37:59 2015 +0200
@@ -155,9 +155,9 @@
let
val _ =
cond_tracing ctxt (fn () =>
- "Resolving clause: " ^ Display.string_of_thm ctxt c1 ^
+ "Resolving clause: " ^ Thm.string_of_thm ctxt c1 ^
" (hyps: " ^ ML_Syntax.print_list (Syntax.string_of_term ctxt) (Thm.hyps_of c1) ^
- ")\nwith clause: " ^ Display.string_of_thm ctxt c2 ^
+ ")\nwith clause: " ^ Thm.string_of_thm ctxt c2 ^
" (hyps: " ^ ML_Syntax.print_list (Syntax.string_of_term ctxt) (Thm.hyps_of c2) ^ ")")
(* the two literals used for resolution *)
@@ -176,7 +176,7 @@
val _ =
cond_tracing ctxt
- (fn () => "Resolution theorem: " ^ Display.string_of_thm ctxt res_thm)
+ (fn () => "Resolution theorem: " ^ Thm.string_of_thm ctxt res_thm)
(* Gamma1, Gamma2 |- False *)
val c_new =
@@ -186,7 +186,7 @@
val _ =
cond_tracing ctxt (fn () =>
- "Resulting clause: " ^ Display.string_of_thm ctxt c_new ^
+ "Resulting clause: " ^ Thm.string_of_thm ctxt c_new ^
" (hyps: " ^
ML_Syntax.print_list (Syntax.string_of_term ctxt) (Thm.hyps_of c_new) ^ ")")
--- a/src/Provers/Arith/fast_lin_arith.ML Fri Sep 25 20:04:25 2015 +0200
+++ b/src/Provers/Arith/fast_lin_arith.ML Fri Sep 25 20:37:59 2015 +0200
@@ -349,7 +349,7 @@
fun trace_thm ctxt msgs th =
(if Config.get ctxt LA_Data.trace
- then tracing (cat_lines (msgs @ [Display.string_of_thm ctxt th]))
+ then tracing (cat_lines (msgs @ [Thm.string_of_thm ctxt th]))
else (); th);
fun trace_term ctxt msgs t =
@@ -468,8 +468,8 @@
if LA_Logic.is_False fls then ()
else
(tracing (cat_lines
- (["Assumptions:"] @ map (Display.string_of_thm ctxt) asms @ [""] @
- ["Proved:", Display.string_of_thm ctxt fls, ""]));
+ (["Assumptions:"] @ map (Thm.string_of_thm ctxt) asms @ [""] @
+ ["Proved:", Thm.string_of_thm ctxt fls, ""]));
warning "Linear arithmetic should have refuted the assumptions.\n\
\Please inform Tobias Nipkow.")
in fls end
--- a/src/Provers/blast.ML Fri Sep 25 20:04:25 2015 +0200
+++ b/src/Provers/blast.ML Fri Sep 25 20:37:59 2015 +0200
@@ -484,7 +484,7 @@
| cond_tracing false _ = ();
fun TRACE ctxt rl tac i st =
- (cond_tracing (Config.get ctxt trace) (fn () => Display.string_of_thm ctxt rl); tac i st);
+ (cond_tracing (Config.get ctxt trace) (fn () => Thm.string_of_thm ctxt rl); tac i st);
(*Resolution/matching tactics: if upd then the proof state may be updated.
Matching makes the tactics more deterministic in the presence of Vars.*)
@@ -509,13 +509,13 @@
handle
ElimBadPrem => (*reject: prems don't preserve conclusion*)
(if Context_Position.is_visible ctxt then
- warning ("Ignoring weak elimination rule\n" ^ Display.string_of_thm ctxt rl0)
+ warning ("Ignoring weak elimination rule\n" ^ Thm.string_of_thm ctxt rl0)
else ();
Option.NONE)
| ElimBadConcl => (*ignore: conclusion is not just a variable*)
(cond_tracing (Config.get ctxt trace)
(fn () => "Ignoring ill-formed elimination rule:\n" ^
- "conclusion should be a variable\n" ^ Display.string_of_thm ctxt rl0);
+ "conclusion should be a variable\n" ^ Thm.string_of_thm ctxt rl0);
Option.NONE);
--- a/src/Provers/classical.ML Fri Sep 25 20:04:25 2015 +0200
+++ b/src/Provers/classical.ML Fri Sep 25 20:37:59 2015 +0200
@@ -282,7 +282,7 @@
fun delete_tagged_list rls = fold_rev Tactic.delete_tagged_brl rls;
fun delete x = delete_tagged_list (joinrules x);
-fun bad_thm ctxt msg th = error (msg ^ "\n" ^ Display.string_of_thm ctxt th);
+fun bad_thm ctxt msg th = error (msg ^ "\n" ^ Thm.string_of_thm ctxt th);
fun make_elim ctxt th =
if has_fewer_prems 1 th then bad_thm ctxt "Ill-formed destruction rule" th
@@ -290,7 +290,7 @@
fun warn_thm ctxt msg th =
if Context_Position.is_really_visible ctxt
- then warning (msg ^ Display.string_of_thm ctxt th) else ();
+ then warning (msg ^ Thm.string_of_thm ctxt th) else ();
fun warn_rules ctxt msg rules (r: rule) =
Item_Net.member rules r andalso (warn_thm ctxt msg (#1 r); true);
@@ -634,7 +634,7 @@
fun print_claset ctxt =
let
val {safeIs, safeEs, unsafeIs, unsafeEs, swrappers, uwrappers, ...} = rep_claset_of ctxt;
- val pretty_thms = map (Display.pretty_thm_item ctxt o #1) o Item_Net.content;
+ val pretty_thms = map (Thm.pretty_thm_item ctxt o #1) o Item_Net.content;
in
[Pretty.big_list "safe introduction rules (intro!):" (pretty_thms safeIs),
Pretty.big_list "introduction rules (intro):" (pretty_thms unsafeIs),
--- a/src/Pure/Isar/attrib.ML Fri Sep 25 20:04:25 2015 +0200
+++ b/src/Pure/Isar/attrib.ML Fri Sep 25 20:37:59 2015 +0200
@@ -532,9 +532,9 @@
register_config Proof_Context.show_abbrevs_raw #>
register_config Goal_Display.goals_limit_raw #>
register_config Goal_Display.show_main_goal_raw #>
- register_config Goal_Display.show_consts_raw #>
- register_config Display.show_hyps_raw #>
- register_config Display.show_tags_raw #>
+ register_config Thm.show_consts_raw #>
+ register_config Thm.show_hyps_raw #>
+ register_config Thm.show_tags_raw #>
register_config Pattern.unify_trace_failure_raw #>
register_config Unify.trace_bound_raw #>
register_config Unify.search_bound_raw #>
--- a/src/Pure/Isar/bundle.ML Fri Sep 25 20:04:25 2015 +0200
+++ b/src/Pure/Isar/bundle.ML Fri Sep 25 20:37:59 2015 +0200
@@ -124,7 +124,7 @@
fun print_bundles verbose ctxt =
let
- val prt_thm = Pretty.backquote o Display.pretty_thm ctxt;
+ val prt_thm = Pretty.backquote o Thm.pretty_thm ctxt;
fun prt_fact (ths, []) = map prt_thm ths
| prt_fact (ths, atts) = Pretty.enclose "(" ")"
--- a/src/Pure/Isar/calculation.ML Fri Sep 25 20:04:25 2015 +0200
+++ b/src/Pure/Isar/calculation.ML Fri Sep 25 20:37:59 2015 +0200
@@ -41,7 +41,7 @@
fun print_rules ctxt =
let
- val pretty_thm = Display.pretty_thm_item ctxt;
+ val pretty_thm = Thm.pretty_thm_item ctxt;
val (trans, sym) = get_rules ctxt;
in
[Pretty.big_list "transitivity rules:" (map pretty_thm (Item_Net.content trans)),
@@ -137,8 +137,8 @@
fun calculate prep_rules final raw_rules int state =
let
val ctxt = Proof.context_of state;
- val pretty_thm = Display.pretty_thm ctxt;
- val pretty_thm_item = Display.pretty_thm_item ctxt;
+ val pretty_thm = Thm.pretty_thm ctxt;
+ val pretty_thm_item = Thm.pretty_thm_item ctxt;
val strip_assums_concl = Logic.strip_assums_concl o Thm.prop_of;
val eq_prop = op aconv o apply2 (Envir.beta_eta_contract o strip_assums_concl);
--- a/src/Pure/Isar/code.ML Fri Sep 25 20:04:25 2015 +0200
+++ b/src/Pure/Isar/code.ML Fri Sep 25 20:37:59 2015 +0200
@@ -443,11 +443,11 @@
exception BAD_THM of string;
fun bad_thm msg = raise BAD_THM msg;
fun error_thm f thy (thm, proper) = f (thm, proper)
- handle BAD_THM msg => error (msg ^ ", in theorem:\n" ^ Display.string_of_thm_global thy thm);
+ handle BAD_THM msg => error (msg ^ ", in theorem:\n" ^ Thm.string_of_thm_global thy thm);
fun error_abs_thm f thy thm = f thm
- handle BAD_THM msg => error (msg ^ ", in theorem:\n" ^ Display.string_of_thm_global thy thm);
+ handle BAD_THM msg => error (msg ^ ", in theorem:\n" ^ Thm.string_of_thm_global thy thm);
fun warning_thm f thy (thm, proper) = SOME (f (thm, proper))
- handle BAD_THM msg => (warning (msg ^ ", in theorem:\n" ^ Display.string_of_thm_global thy thm); NONE)
+ handle BAD_THM msg => (warning (msg ^ ", in theorem:\n" ^ Thm.string_of_thm_global thy thm); NONE)
fun try_thm f thm_proper = SOME (f thm_proper)
handle BAD_THM _ => NONE;
@@ -764,7 +764,7 @@
val (thms, propers) = split_list eqns;
val _ = map (fn thm => if c = const_eqn thy thm then ()
else error ("Wrong head of code equation,\nexpected constant "
- ^ string_of_const thy c ^ "\n" ^ Display.string_of_thm_global thy thm)) thms;
+ ^ string_of_const thy c ^ "\n" ^ Thm.string_of_thm_global thy thm)) thms;
fun tvars_of T = rev (Term.add_tvarsT T []);
val vss = map (tvars_of o snd o head_eqn) thms;
fun inter_sorts vs =
@@ -794,7 +794,7 @@
val _ = assert_abs_eqn thy (SOME tyco) abs_thm;
val _ = if c = const_abs_eqn thy abs_thm then ()
else error ("Wrong head of abstract code equation,\nexpected constant "
- ^ string_of_const thy c ^ "\n" ^ Display.string_of_thm_global thy abs_thm);
+ ^ string_of_const thy c ^ "\n" ^ Thm.string_of_thm_global thy abs_thm);
in Abstract (Thm.legacy_freezeT abs_thm, tyco) end;
fun constrain_cert_thm thy sorts cert_thm =
@@ -888,12 +888,12 @@
fun pretty_cert thy (cert as Nothing _) =
[Pretty.str "(not implemented)"]
| pretty_cert thy (cert as Equations _) =
- (map_filter (Option.map (Display.pretty_thm_global thy o Axclass.overload thy) o fst o snd)
+ (map_filter (Option.map (Thm.pretty_thm_global thy o Axclass.overload thy) o fst o snd)
o these o snd o equations_of_cert thy) cert
| pretty_cert thy (Projection (t, _)) =
[Syntax.pretty_term_global thy (Logic.varify_types_global t)]
| pretty_cert thy (Abstract (abs_thm, _)) =
- [(Display.pretty_thm_global thy o Axclass.overload thy o Thm.varifyT_global) abs_thm];
+ [(Thm.pretty_thm_global thy o Axclass.overload thy o Thm.varifyT_global) abs_thm];
end;
@@ -927,7 +927,7 @@
fun cert_of_eqns_preprocess ctxt functrans c =
let
fun trace_eqns s eqns = (Pretty.writeln o Pretty.chunks)
- (Pretty.str s :: map (Display.pretty_thm ctxt o fst) eqns);
+ (Pretty.str s :: map (Thm.pretty_thm ctxt o fst) eqns);
val tracing = if Config.get ctxt simp_trace then trace_eqns else (K o K) ();
in
tap (tracing "before function transformation")
@@ -1010,7 +1010,7 @@
val exec = the_exec thy;
fun pretty_equations const thms =
(Pretty.block o Pretty.fbreaks)
- (Pretty.str (string_of_const thy const) :: map (Display.pretty_thm_item ctxt) thms);
+ (Pretty.str (string_of_const thy const) :: map (Thm.pretty_thm_item ctxt) thms);
fun pretty_function (const, Eqns_Default (_, eqns_lazy)) =
pretty_equations const (map fst (Lazy.force eqns_lazy))
| pretty_function (const, Eqns eqns) = pretty_equations const (map fst eqns)
@@ -1096,7 +1096,7 @@
fun drop (thm', proper') = if (proper orelse not proper')
andalso matches_args (args_of thm') then
(if verbose then warning ("Code generator: dropping subsumed code equation\n" ^
- Display.string_of_thm_global thy thm') else (); true)
+ Thm.string_of_thm_global thy thm') else (); true)
else false;
in (thm, proper) :: filter_out drop eqns end;
fun natural_order eqns =
--- a/src/Pure/Isar/context_rules.ML Fri Sep 25 20:04:25 2015 +0200
+++ b/src/Pure/Isar/context_rules.ML Fri Sep 25 20:37:59 2015 +0200
@@ -121,7 +121,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 (Display.pretty_thm_item ctxt th) else NONE)
+ if k = (i, b) then SOME (Thm.pretty_thm_item ctxt th) else NONE)
(sort (int_ord o apply2 fst) rules));
in Pretty.writeln_chunks (map prt_kind rule_kinds) end;
--- a/src/Pure/Isar/element.ML Fri Sep 25 20:04:25 2015 +0200
+++ b/src/Pure/Isar/element.ML Fri Sep 25 20:37:59 2015 +0200
@@ -152,7 +152,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 Display.pretty_thm ctxt;
+ val prt_thm = Pretty.backquote o Thm.pretty_thm ctxt;
fun prt_binding (b, atts) =
Attrib.pretty_binding ctxt (b, if show_attribs then atts else []);
--- a/src/Pure/Isar/local_defs.ML Fri Sep 25 20:04:25 2015 +0200
+++ b/src/Pure/Isar/local_defs.ML Fri Sep 25 20:37:59 2015 +0200
@@ -176,7 +176,7 @@
fun print_rules ctxt =
Pretty.writeln (Pretty.big_list "definitional rewrite rules:"
- (map (Display.pretty_thm_item ctxt) (Rules.get (Context.Proof ctxt))));
+ (map (Thm.pretty_thm_item ctxt) (Rules.get (Context.Proof ctxt))));
val defn_add = Thm.declaration_attribute (Rules.map o Thm.add_thm o Thm.trim_context);
val defn_del = Thm.declaration_attribute (Rules.map o Thm.del_thm o Thm.trim_context);
--- a/src/Pure/Isar/method.ML Fri Sep 25 20:04:25 2015 +0200
+++ b/src/Pure/Isar/method.ML Fri Sep 25 20:37:59 2015 +0200
@@ -218,7 +218,7 @@
fun trace ctxt rules =
if Config.get ctxt rule_trace andalso not (null rules) then
- Pretty.big_list "rules:" (map (Display.pretty_thm_item ctxt) rules)
+ Pretty.big_list "rules:" (map (Thm.pretty_thm_item ctxt) rules)
|> Pretty.string_of |> tracing
else ();
--- a/src/Pure/Isar/obtain.ML Fri Sep 25 20:04:25 2015 +0200
+++ b/src/Pure/Isar/obtain.ML Fri Sep 25 20:37:59 2015 +0200
@@ -257,9 +257,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" ^ Display.string_of_thm ctxt th)
+ else error ("Guessed a different clause:\n" ^ Thm.string_of_thm ctxt th)
| [] => error "Goal solved -- nothing guessed"
- | _ => error ("Guess split into several cases:\n" ^ Display.string_of_thm ctxt th));
+ | _ => error ("Guess split into several cases:\n" ^ Thm.string_of_thm ctxt th));
fun result tac facts ctxt =
let
@@ -308,7 +308,7 @@
val thy = Proof_Context.theory_of ctxt;
val string_of_term = Syntax.string_of_term (Config.put show_types true ctxt);
- fun err msg th = error (msg ^ ":\n" ^ Display.string_of_thm ctxt th);
+ fun err msg th = error (msg ^ ":\n" ^ Thm.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 Fri Sep 25 20:04:25 2015 +0200
+++ b/src/Pure/Isar/proof.ML Fri Sep 25 20:37:59 2015 +0200
@@ -495,7 +495,7 @@
error "Bad background theory of goal state";
val _ = Thm.no_prems goal orelse error (Proof_Display.string_of_goal ctxt goal);
- fun err_lost () = error ("Lost goal structure:\n" ^ Display.string_of_thm ctxt goal);
+ fun err_lost () = error ("Lost goal structure:\n" ^ Thm.string_of_thm ctxt goal);
val th =
(Goal.conclude (if length (flat propss) > 1 then Thm.close_derivation goal else goal)
@@ -511,7 +511,7 @@
handle THM _ => err_lost ();
val _ =
Unify.matches_list (Context.Proof ctxt) (flat goal_propss) (map Thm.prop_of (flat results))
- orelse error ("Proved a different theorem:\n" ^ Display.string_of_thm ctxt th);
+ orelse error ("Proved a different theorem:\n" ^ Thm.string_of_thm ctxt th);
fun recover_result ([] :: pss) thss = [] :: recover_result pss thss
| recover_result (_ :: pss) (ths :: thss) = ths :: recover_result pss thss
--- a/src/Pure/Isar/proof_context.ML Fri Sep 25 20:04:25 2015 +0200
+++ b/src/Pure/Isar/proof_context.ML Fri Sep 25 20:37:59 2015 +0200
@@ -396,8 +396,8 @@
fun pretty_fact ctxt =
let
- val pretty_thm = Display.pretty_thm ctxt;
- val pretty_thms = map (Display.pretty_thm_item ctxt);
+ val pretty_thm = Thm.pretty_thm ctxt;
+ val pretty_thms = map (Thm.pretty_thm_item ctxt);
in
fn ("", [th]) => pretty_thm th
| ("", ths) => Pretty.blk (0, Pretty.fbreaks (pretty_thms ths))
--- a/src/Pure/Isar/proof_display.ML Fri Sep 25 20:04:25 2015 +0200
+++ b/src/Pure/Isar/proof_display.ML Fri Sep 25 20:37:59 2015 +0200
@@ -48,7 +48,7 @@
| NONE => Syntax.init_pretty_global (mk_thy ()));
fun pp_thm mk_thy th =
- Display.pretty_thm_raw (default_context mk_thy) {quote = true, show_hyps = false} th;
+ Thm.pretty_thm_raw (default_context mk_thy) {quote = true, show_hyps = false} th;
fun pp_typ mk_thy T = Pretty.quote (Syntax.pretty_typ (default_context mk_thy) T);
fun pp_term mk_thy t = Pretty.quote (Syntax.pretty_term (default_context mk_thy) t);
@@ -215,7 +215,7 @@
fun pretty_rule ctxt s thm =
Pretty.block [Pretty.str (s ^ " attempt to solve goal by exported rule:"),
- Pretty.fbrk, Display.pretty_thm ctxt thm];
+ Pretty.fbrk, Thm.pretty_thm ctxt thm];
val string_of_rule = Pretty.string_of ooo pretty_rule;
--- a/src/Pure/Isar/runtime.ML Fri Sep 25 20:04:25 2015 +0200
+++ b/src/Pure/Isar/runtime.ML Fri Sep 25 20:37:59 2015 +0200
@@ -119,7 +119,7 @@
(msg :: robust_context context Syntax.string_of_term (map Thm.term_of cts))
| THM (msg, i, thms) =>
raised exn ("THM " ^ string_of_int i)
- (msg :: robust_context context Display.string_of_thm thms)
+ (msg :: robust_context context Thm.string_of_thm thms)
| _ => raised exn (robust (Pretty.string_of o Exn_Output.pretty) exn) []);
in [((i, msg), id)] end)
and sorted_msgs context exn =
--- a/src/Pure/Isar/token.ML Fri Sep 25 20:04:25 2015 +0200
+++ b/src/Pure/Isar/token.ML Fri Sep 25 20:37:59 2015 +0200
@@ -498,7 +498,7 @@
| SOME (Typ T) => Syntax.pretty_typ ctxt T
| SOME (Term t) => Syntax.pretty_term ctxt t
| SOME (Fact (_, ths)) =>
- Pretty.enclose "(" ")" (Pretty.breaks (map (Pretty.backquote o Display.pretty_thm ctxt) ths))
+ Pretty.enclose "(" ")" (Pretty.breaks (map (Pretty.backquote o Thm.pretty_thm ctxt) ths))
| _ => Pretty.marks_str (markups Keyword.empty_keywords tok, unparse tok));
fun pretty_src ctxt src =
--- a/src/Pure/Proof/reconstruct.ML Fri Sep 25 20:04:25 2015 +0200
+++ b/src/Pure/Proof/reconstruct.ML Fri Sep 25 20:37:59 2015 +0200
@@ -254,8 +254,8 @@
let
fun search env [] = error ("Unsolvable constraints:\n" ^
Pretty.string_of (Pretty.chunks (map (fn (_, p, _) =>
- Goal_Display.pretty_flexpair (Syntax.init_pretty_global thy) (apply2
- (Envir.norm_term bigenv) p)) cs)))
+ Thm.pretty_flexpair (Syntax.init_pretty_global thy)
+ (apply2 (Envir.norm_term bigenv) p)) cs)))
| search env ((u, p as (t1, t2), vs)::ps) =
if u then
let
--- a/src/Pure/ROOT Fri Sep 25 20:04:25 2015 +0200
+++ b/src/Pure/ROOT Fri Sep 25 20:37:59 2015 +0200
@@ -247,7 +247,6 @@
"context_position.ML"
"conv.ML"
"defs.ML"
- "display.ML"
"drule.ML"
"envir.ML"
"facts.ML"
--- a/src/Pure/ROOT.ML Fri Sep 25 20:04:25 2015 +0200
+++ b/src/Pure/ROOT.ML Fri Sep 25 20:37:59 2015 +0200
@@ -195,7 +195,6 @@
use "raw_simplifier.ML";
use "conjunction.ML";
use "assumption.ML";
-use "display.ML";
(* Isar -- Intelligible Semi-Automated Reasoning *)
--- a/src/Pure/Tools/find_theorems.ML Fri Sep 25 20:04:25 2015 +0200
+++ b/src/Pure/Tools/find_theorems.ML Fri Sep 25 20:37:59 2015 +0200
@@ -462,7 +462,7 @@
in
fun pretty_thm ctxt (thmref, thm) =
- Pretty.block (pretty_ref ctxt thmref @ [Display.pretty_thm ctxt thm]);
+ Pretty.block (pretty_ref ctxt thmref @ [Thm.pretty_thm ctxt thm]);
fun pretty_theorems state opt_limit rem_dups raw_criteria =
let
--- a/src/Pure/display.ML Fri Sep 25 20:04:25 2015 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,91 +0,0 @@
-(* Title: Pure/display.ML
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Author: Makarius
-
-Printing of theorems, results etc.
-*)
-
-signature BASIC_DISPLAY =
-sig
- val show_consts: bool Config.T
- val show_hyps_raw: Config.raw
- val show_hyps: bool Config.T
- val show_tags_raw: Config.raw
- val show_tags: bool Config.T
-end;
-
-signature DISPLAY =
-sig
- include BASIC_DISPLAY
- val pretty_thm_raw: Proof.context -> {quote: bool, show_hyps: bool} -> thm -> Pretty.T
- val pretty_thm: Proof.context -> thm -> Pretty.T
- val pretty_thm_item: Proof.context -> thm -> Pretty.T
- val pretty_thm_global: theory -> thm -> Pretty.T
- val string_of_thm: Proof.context -> thm -> string
- val string_of_thm_global: theory -> thm -> string
-end;
-
-structure Display: DISPLAY =
-struct
-
-(** options **)
-
-val show_consts = Goal_Display.show_consts;
-
-val show_hyps_raw = Config.declare ("show_hyps", @{here}) (fn _ => Config.Bool false);
-val show_hyps = Config.bool show_hyps_raw;
-
-val show_tags_raw = Config.declare ("show_tags", @{here}) (fn _ => Config.Bool false);
-val show_tags = Config.bool show_tags_raw;
-
-
-
-(** print thm **)
-
-fun pretty_tag (name, arg) = Pretty.strs [name, quote arg];
-val pretty_tags = Pretty.list "[" "]" o map pretty_tag;
-
-fun pretty_thm_raw ctxt {quote, show_hyps = show_hyps'} raw_th =
- let
- val show_tags = Config.get ctxt show_tags;
- val show_hyps = Config.get ctxt show_hyps;
-
- val th = raw_th
- |> perhaps (try (Thm.transfer (Proof_Context.theory_of ctxt)))
- |> perhaps (try Thm.strip_shyps);
-
- val hyps = if show_hyps then Thm.hyps_of th else Thm.undeclared_hyps (Context.Proof ctxt) th;
- val extra_shyps = Thm.extra_shyps th;
- val tags = Thm.get_tags th;
- val tpairs = Thm.tpairs_of th;
-
- val q = if quote then Pretty.quote else I;
- val prt_term = q o Syntax.pretty_term ctxt;
-
-
- val hlen = length extra_shyps + length hyps + length tpairs;
- val hsymbs =
- if hlen = 0 then []
- else if show_hyps orelse show_hyps' then
- [Pretty.brk 2, Pretty.list "[" "]"
- (map (q o Goal_Display.pretty_flexpair ctxt) tpairs @ map prt_term hyps @
- map (Syntax.pretty_sort ctxt) extra_shyps)]
- else [Pretty.brk 2, Pretty.str ("[" ^ replicate_string hlen "." ^ "]")];
- val tsymbs =
- if null tags orelse not show_tags then []
- else [Pretty.brk 1, pretty_tags tags];
- in Pretty.block (prt_term (Thm.prop_of th) :: (hsymbs @ tsymbs)) end;
-
-fun pretty_thm ctxt = pretty_thm_raw ctxt {quote = false, show_hyps = true};
-fun pretty_thm_item ctxt th = Pretty.item [pretty_thm ctxt th];
-
-fun pretty_thm_global thy =
- pretty_thm_raw (Syntax.init_pretty_global thy) {quote = false, show_hyps = false};
-
-val string_of_thm = Pretty.string_of oo pretty_thm;
-val string_of_thm_global = Pretty.string_of oo pretty_thm_global;
-
-end;
-
-structure Basic_Display: BASIC_DISPLAY = Display;
-open Basic_Display;
--- a/src/Pure/goal_display.ML Fri Sep 25 20:04:25 2015 +0200
+++ b/src/Pure/goal_display.ML Fri Sep 25 20:37:59 2015 +0200
@@ -11,9 +11,6 @@
val goals_limit: int Config.T
val show_main_goal_raw: Config.raw
val show_main_goal: bool Config.T
- val show_consts_raw: Config.raw
- val show_consts: bool Config.T
- val pretty_flexpair: Proof.context -> term * term -> Pretty.T
val pretty_goals: Proof.context -> thm -> Pretty.T list
val pretty_goal: Proof.context -> thm -> Pretty.T
val string_of_goal: Proof.context -> thm -> string
@@ -28,12 +25,6 @@
val show_main_goal_raw = Config.declare_option ("show_main_goal", @{here});
val show_main_goal = Config.bool show_main_goal_raw;
-val show_consts_raw = Config.declare_option ("show_consts", @{here});
-val show_consts = Config.bool show_consts_raw;
-
-fun pretty_flexpair ctxt (t, u) = Pretty.block
- [Syntax.pretty_term ctxt t, Pretty.str " =?=", Pretty.brk 1, Syntax.pretty_term ctxt u];
-
(*print thm A1,...,An/B in "goal style" -- premises as numbered subgoals*)
@@ -107,7 +98,7 @@
Pretty.markup (Markup.subgoal s) [Pretty.str (" " ^ s ^ ". "), prt_term A];
val pretty_subgoals = map_index (fn (i, A) => pretty_subgoal (string_of_int (i + 1)) A);
- val pretty_ffpairs = pretty_list "flex-flex pairs:" (pretty_flexpair ctxt);
+ val pretty_ffpairs = pretty_list "flex-flex pairs:" (Thm.pretty_flexpair ctxt);
val pretty_consts = pretty_list "constants:" prt_consts o consts_of;
val pretty_vars = pretty_list "variables:" prt_vars o vars_of;
--- a/src/Pure/more_thm.ML Fri Sep 25 20:04:25 2015 +0200
+++ b/src/Pure/more_thm.ML Fri Sep 25 20:37:59 2015 +0200
@@ -9,6 +9,9 @@
signature BASIC_THM =
sig
include BASIC_THM
+ val show_consts: bool Config.T
+ val show_hyps: bool Config.T
+ val show_tags: bool Config.T
structure Ctermtab: TABLE
structure Thmtab: TABLE
val aconvc: cterm * cterm -> bool
@@ -105,6 +108,19 @@
val kind: string -> attribute
val register_proofs: thm list -> theory -> theory
val join_theory_proofs: theory -> unit
+ val show_consts_raw: Config.raw
+ val show_consts: bool Config.T
+ val show_hyps_raw: Config.raw
+ val show_hyps: bool Config.T
+ val show_tags_raw: Config.raw
+ val show_tags: bool Config.T
+ val pretty_flexpair: Proof.context -> term * term -> Pretty.T
+ val pretty_thm_raw: Proof.context -> {quote: bool, show_hyps: bool} -> thm -> Pretty.T
+ val pretty_thm: Proof.context -> thm -> Pretty.T
+ val pretty_thm_item: Proof.context -> thm -> Pretty.T
+ val pretty_thm_global: theory -> thm -> Pretty.T
+ val string_of_thm: Proof.context -> thm -> string
+ val string_of_thm_global: theory -> thm -> string
end;
structure Thm: THM =
@@ -586,6 +602,70 @@
Thm.join_proofs (map (Thm.transfer thy) (rev (Proofs.get thy)));
+
+(** print theorems **)
+
+(* options *)
+
+val show_consts_raw = Config.declare_option ("show_consts", @{here});
+val show_consts = Config.bool show_consts_raw;
+
+val show_hyps_raw = Config.declare ("show_hyps", @{here}) (fn _ => Config.Bool false);
+val show_hyps = Config.bool show_hyps_raw;
+
+val show_tags_raw = Config.declare ("show_tags", @{here}) (fn _ => Config.Bool false);
+val show_tags = Config.bool show_tags_raw;
+
+
+(* pretty_thm etc. *)
+
+fun pretty_tag (name, arg) = Pretty.strs [name, quote arg];
+val pretty_tags = Pretty.list "[" "]" o map pretty_tag;
+
+fun pretty_flexpair ctxt (t, u) = Pretty.block
+ [Syntax.pretty_term ctxt t, Pretty.str " =?=", Pretty.brk 1, Syntax.pretty_term ctxt u];
+
+fun pretty_thm_raw ctxt {quote, show_hyps = show_hyps'} raw_th =
+ let
+ val show_tags = Config.get ctxt show_tags;
+ val show_hyps = Config.get ctxt show_hyps;
+
+ val th = raw_th
+ |> perhaps (try (Thm.transfer (Proof_Context.theory_of ctxt)))
+ |> perhaps (try Thm.strip_shyps);
+
+ val hyps = if show_hyps then Thm.hyps_of th else undeclared_hyps (Context.Proof ctxt) th;
+ val extra_shyps = Thm.extra_shyps th;
+ val tags = Thm.get_tags th;
+ val tpairs = Thm.tpairs_of th;
+
+ val q = if quote then Pretty.quote else I;
+ val prt_term = q o Syntax.pretty_term ctxt;
+
+
+ val hlen = length extra_shyps + length hyps + length tpairs;
+ val hsymbs =
+ if hlen = 0 then []
+ else if show_hyps orelse show_hyps' then
+ [Pretty.brk 2, Pretty.list "[" "]"
+ (map (q o pretty_flexpair ctxt) tpairs @ map prt_term hyps @
+ map (Syntax.pretty_sort ctxt) extra_shyps)]
+ else [Pretty.brk 2, Pretty.str ("[" ^ replicate_string hlen "." ^ "]")];
+ val tsymbs =
+ if null tags orelse not show_tags then []
+ else [Pretty.brk 1, pretty_tags tags];
+ in Pretty.block (prt_term (Thm.prop_of th) :: (hsymbs @ tsymbs)) end;
+
+fun pretty_thm ctxt = pretty_thm_raw ctxt {quote = false, show_hyps = true};
+fun pretty_thm_item ctxt th = Pretty.item [pretty_thm ctxt th];
+
+fun pretty_thm_global thy =
+ pretty_thm_raw (Syntax.init_pretty_global thy) {quote = false, show_hyps = false};
+
+val string_of_thm = Pretty.string_of oo pretty_thm;
+val string_of_thm_global = Pretty.string_of oo pretty_thm_global;
+
+
open Thm;
end;
--- a/src/Pure/simplifier.ML Fri Sep 25 20:04:25 2015 +0200
+++ b/src/Pure/simplifier.ML Fri Sep 25 20:37:59 2015 +0200
@@ -162,8 +162,8 @@
fun pretty_simpset verbose ctxt =
let
val pretty_term = Syntax.pretty_term ctxt;
- val pretty_thm = Display.pretty_thm ctxt;
- val pretty_thm_item = Display.pretty_thm_item ctxt;
+ val pretty_thm = Thm.pretty_thm ctxt;
+ val pretty_thm_item = Thm.pretty_thm_item ctxt;
fun pretty_simproc (name, lhss) =
Pretty.block
--- a/src/Sequents/prover.ML Fri Sep 25 20:04:25 2015 +0200
+++ b/src/Sequents/prover.ML Fri Sep 25 20:37:59 2015 +0200
@@ -63,8 +63,8 @@
fun pretty_pack ctxt =
let val (safes, unsafes) = get_rules ctxt in
Pretty.chunks
- [Pretty.big_list "safe rules:" (map (Display.pretty_thm ctxt) safes),
- Pretty.big_list "unsafe rules:" (map (Display.pretty_thm ctxt) unsafes)]
+ [Pretty.big_list "safe rules:" (map (Thm.pretty_thm ctxt) safes),
+ Pretty.big_list "unsafe rules:" (map (Thm.pretty_thm ctxt) unsafes)]
end;
val _ =
@@ -82,7 +82,7 @@
(case context of
Context.Proof ctxt =>
if Context_Position.is_really_visible ctxt then
- warning ("Ignoring duplicate theorems:\n" ^ Display.string_of_thm ctxt th)
+ warning ("Ignoring duplicate theorems:\n" ^ Thm.string_of_thm ctxt th)
else ()
| _ => ());
in ths end
--- a/src/Sequents/simpdata.ML Fri Sep 25 20:04:25 2015 +0200
+++ b/src/Sequents/simpdata.ML Fri Sep 25 20:37:59 2015 +0200
@@ -38,7 +38,7 @@
| (Const(@{const_name iff},_)$_$_) => th RS @{thm iff_reflection}
| (Const(@{const_name Not},_)$_) => th RS @{thm iff_reflection_F}
| _ => th RS @{thm iff_reflection_T})
- | _ => error ("addsimps: unable to use theorem\n" ^ Display.string_of_thm ctxt th));
+ | _ => error ("addsimps: unable to use theorem\n" ^ Thm.string_of_thm ctxt th));
(*Replace premises x=y, X<->Y by X==Y*)
fun mk_meta_prems ctxt =
--- a/src/Tools/Code/code_printer.ML Fri Sep 25 20:04:25 2015 +0200
+++ b/src/Tools/Code/code_printer.ML Fri Sep 25 20:37:59 2015 +0200
@@ -111,7 +111,7 @@
(** generic nonsense *)
fun eqn_error thy (SOME thm) s =
- error (s ^ ",\nin equation " ^ Display.string_of_thm_global thy thm)
+ error (s ^ ",\nin equation " ^ Thm.string_of_thm_global thy thm)
| eqn_error _ NONE s = error s;
val code_presentationN = "code_presentation";
--- a/src/Tools/Code/code_thingol.ML Fri Sep 25 20:04:25 2015 +0200
+++ b/src/Tools/Code/code_thingol.ML Fri Sep 25 20:37:59 2015 +0200
@@ -396,7 +396,7 @@
else
let
val thm_msg =
- Option.map (fn thm => "in code equation " ^ Display.string_of_thm ctxt thm) some_thm;
+ Option.map (fn thm => "in code equation " ^ Thm.string_of_thm ctxt thm) some_thm;
val dep_msg = if null (tl deps) then NONE
else SOME ("with dependency "
^ space_implode " -> " (map (Code_Symbol.quote ctxt) (rev deps)));
--- a/src/Tools/coherent.ML Fri Sep 25 20:04:25 2015 +0200
+++ b/src/Tools/coherent.ML Fri Sep 25 20:37:59 2015 +0200
@@ -175,7 +175,7 @@
let
val _ =
cond_trace ctxt (fn () =>
- Pretty.string_of (Pretty.big_list "asms:" (map (Display.pretty_thm ctxt) asms)));
+ Pretty.string_of (Pretty.big_list "asms:" (map (Thm.pretty_thm ctxt) asms)));
val th' =
Drule.implies_elim_list
(Thm.instantiate
--- a/src/Tools/induct.ML Fri Sep 25 20:04:25 2015 +0200
+++ b/src/Tools/induct.ML Fri Sep 25 20:37:59 2015 +0200
@@ -207,7 +207,7 @@
fun pretty_rules ctxt kind rs =
let val thms = map snd (Item_Net.content rs)
- in Pretty.big_list kind (map (Display.pretty_thm_item ctxt) thms) end;
+ in Pretty.big_list kind (map (Thm.pretty_thm_item ctxt) thms) end;
(* context data *)
--- a/src/Tools/nbe.ML Fri Sep 25 20:04:25 2015 +0200
+++ b/src/Tools/nbe.ML Fri Sep 25 20:37:59 2015 +0200
@@ -50,17 +50,17 @@
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_global thy thm);
+ | _ => error ("Bad certificate: " ^ Thm.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_global thy thm);
+ | _ => error ("Bad certificate: " ^ Thm.string_of_thm_global thy thm);
val tvar = case try Term.dest_TVar T
of SOME (tvar as (_, sort)) => if null (filter (can (Axclass.get_info thy)) sort)
then tvar
- else error ("Bad sort: " ^ Display.string_of_thm_global thy thm)
- | _ => error ("Bad type: " ^ Display.string_of_thm_global thy thm);
+ else error ("Bad sort: " ^ Thm.string_of_thm_global thy thm)
+ | _ => error ("Bad type: " ^ Thm.string_of_thm_global thy thm);
val _ = if Term.add_tvars eqn [] = [tvar] then ()
- else error ("Inconsistent type: " ^ Display.string_of_thm_global thy thm);
+ else error ("Inconsistent type: " ^ Thm.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);
@@ -69,7 +69,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_global thy thm);
+ else error ("Inconsistent class: " ^ Thm.string_of_thm_global thy thm);
in Triv_Class_Data.map (AList.update (op =) (class, Thm.trim_context thm)) thy end;
local
--- a/src/ZF/Tools/inductive_package.ML Fri Sep 25 20:04:25 2015 +0200
+++ b/src/ZF/Tools/inductive_package.ML Fri Sep 25 20:37:59 2015 +0200
@@ -319,7 +319,7 @@
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]))
+ ["raw_induct:", Thm.string_of_thm ctxt1 raw_induct]))
else ();
@@ -352,7 +352,7 @@
val dummy =
if ! Ind_Syntax.trace then
- writeln ("quant_induct:\n" ^ Display.string_of_thm ctxt1 quant_induct)
+ writeln ("quant_induct:\n" ^ Thm.string_of_thm ctxt1 quant_induct)
else ();
@@ -429,7 +429,7 @@
val dummy =
if ! Ind_Syntax.trace then
- writeln ("lemma: " ^ Display.string_of_thm ctxt1 lemma)
+ writeln ("lemma: " ^ Thm.string_of_thm ctxt1 lemma)
else ();
--- a/src/ZF/Tools/typechk.ML Fri Sep 25 20:04:25 2015 +0200
+++ b/src/ZF/Tools/typechk.ML Fri Sep 25 20:37:59 2015 +0200
@@ -26,7 +26,7 @@
fun add_rule ctxt 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 ctxt th); tcs)
+ (warning ("Ignoring duplicate type-checking rule\n" ^ Thm.string_of_thm ctxt th); tcs)
else
TC {rules = th :: rules, net = Net.insert_term (K false) (Thm.concl_of th, th) net};
@@ -34,7 +34,7 @@
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 ctxt th); tcs);
+ else (warning ("No such type-checking rule\n" ^ Thm.string_of_thm ctxt th); tcs);
(* generic data *)
@@ -61,7 +61,7 @@
fun print_tcset ctxt =
let val TC {rules, ...} = tcset_of ctxt in
Pretty.writeln (Pretty.big_list "type-checking rules:"
- (map (Display.pretty_thm_item ctxt) rules))
+ (map (Thm.pretty_thm_item ctxt) rules))
end;