--- a/src/HOL/Tools/induct_method.ML Sun Sep 17 22:19:02 2000 +0200
+++ b/src/HOL/Tools/induct_method.ML Sun Sep 17 22:21:31 2000 +0200
@@ -47,9 +47,9 @@
fun lookup_rule (rs:rules) name = Library.assoc (NetRules.rules rs, name);
-fun print_rules kind rs =
+fun print_rules kind sg rs =
let val thms = map snd (NetRules.rules rs)
- in Pretty.writeln (Pretty.big_list kind (map Display.pretty_thm thms)) end;
+ in Pretty.writeln (Pretty.big_list kind (map (Display.pretty_thm_sg sg) thms)) end;
(* theory data kind 'HOL/induct_method' *)
@@ -67,11 +67,11 @@
((NetRules.merge (casesT1, casesT2), NetRules.merge (casesS1, casesS2)),
(NetRules.merge (inductT1, inductT2), NetRules.merge (inductS1, inductS2)));
- fun print _ ((casesT, casesS), (inductT, inductS)) =
- (print_rules "type cases:" casesT;
- print_rules "set cases:" casesS;
- print_rules "type induct:" inductT;
- print_rules "set induct:" inductS);
+ fun print sg ((casesT, casesS), (inductT, inductS)) =
+ (print_rules "type cases:" sg casesT;
+ print_rules "set cases:" sg casesS;
+ print_rules "type induct:" sg inductT;
+ print_rules "set induct:" sg inductS);
fun dest ((casesT, casesS), (inductT, inductS)) =
{type_cases = NetRules.rules casesT,
@@ -93,7 +93,7 @@
type T = GlobalInductArgs.T;
fun init thy = GlobalInduct.get thy;
- fun print x = GlobalInductArgs.print x;
+ val print = GlobalInductArgs.print o ProofContext.sign_of;
end;
structure LocalInduct = ProofDataFun(LocalInductArgs);
--- a/src/HOL/Tools/inductive_package.ML Sun Sep 17 22:19:02 2000 +0200
+++ b/src/HOL/Tools/inductive_package.ML Sun Sep 17 22:21:31 2000 +0200
@@ -81,7 +81,7 @@
fun print sg (tab, monos) =
[Pretty.strs ("(co)inductives:" :: map #1 (Sign.cond_extern_table sg Sign.constK tab)),
- Pretty.big_list "monotonicity rules:" (map Display.pretty_thm monos)]
+ Pretty.big_list "monotonicity rules:" (map (Display.pretty_thm_sg sg) monos)]
|> Pretty.chunks |> Pretty.writeln;
end;
--- a/src/HOL/Tools/record_package.ML Sun Sep 17 22:19:02 2000 +0200
+++ b/src/HOL/Tools/record_package.ML Sun Sep 17 22:21:31 2000 +0200
@@ -828,8 +828,8 @@
("make_defs", make_defs),
("select_convs", sel_convs),
("update_convs", update_convs)]
- |> (#1 oo (PureThy.add_thms o map Thm.no_attributes))
- [("equality", equality)]
+ |> (#1 oo PureThy.add_thms)
+ [(("equality", equality), [Classical.xtra_intro_global])]
|> (#1 oo PureThy.add_thmss)
[(("simps", simps), [Simplifier.simp_add_global]),
(("iffs", iffs), [iff_add_global])];
--- a/src/Pure/Isar/calculation.ML Sun Sep 17 22:19:02 2000 +0200
+++ b/src/Pure/Isar/calculation.ML Sun Sep 17 22:21:31 2000 +0200
@@ -28,8 +28,8 @@
(* theory data kind 'Isar/calculation' *)
-fun print_rules rs = Pretty.writeln (Pretty.big_list "transitivity rules:"
- (map Display.pretty_thm (NetRules.rules rs)));
+fun print_rules sg rs = Pretty.writeln (Pretty.big_list "transitivity rules:"
+ (map (Display.pretty_thm_sg sg) (NetRules.rules rs)));
structure GlobalCalculationArgs =
struct
@@ -40,7 +40,7 @@
val copy = I;
val prep_ext = I;
val merge = NetRules.merge;
- fun print _ = print_rules;
+ val print = print_rules;
end;
structure GlobalCalculation = TheoryDataFun(GlobalCalculationArgs);
@@ -55,7 +55,7 @@
type T = thm NetRules.T * (thm list * int) option;
fun init thy = (GlobalCalculation.get thy, None);
- fun print _ (rs, _) = print_rules rs;
+ fun print ctxt (rs, _) = print_rules (ProofContext.sign_of ctxt) rs;
end;
structure LocalCalculation = ProofDataFun(LocalCalculationArgs);
--- a/src/Pure/Isar/method.ML Sun Sep 17 22:19:02 2000 +0200
+++ b/src/Pure/Isar/method.ML Sun Sep 17 22:21:31 2000 +0200
@@ -127,11 +127,14 @@
(** global and local rule data **)
-fun prt_rules kind ths =
- Pretty.writeln (Pretty.big_list ("standard " ^ kind ^ " rules:") (map Display.pretty_thm ths));
-
-fun print_rules (intro, elim) =
- (prt_rules "introduction" intro; prt_rules "elimination" elim);
+local
+ fun prt_rules kind sg ths =
+ Pretty.writeln (Pretty.big_list ("standard " ^ kind ^ " rules:")
+ (map (Display.pretty_thm_sg sg) ths));
+in
+ fun print_rules sg (intro, elim) =
+ (prt_rules "introduction" sg intro; prt_rules "elimination" sg elim);
+end;
(* theory data kind 'Isar/rules' *)
@@ -146,7 +149,7 @@
val prep_ext = I;
fun merge ((intro1, elim1), (intro2, elim2)) =
(Drule.merge_rules (intro1, intro2), Drule.merge_rules (elim1, elim2));
- fun print _ = print_rules;
+ val print = print_rules;
end;
structure GlobalRules = TheoryDataFun(GlobalRulesArgs);
@@ -161,7 +164,7 @@
type T = thm list * thm list;
val init = GlobalRules.get;
- fun print _ = print_rules;
+ val print = print_rules o ProofContext.sign_of;
end;
structure LocalRules = ProofDataFun(LocalRulesArgs);
--- a/src/Pure/axclass.ML Sun Sep 17 22:19:02 2000 +0200
+++ b/src/Pure/axclass.ML Sun Sep 17 22:21:31 2000 +0200
@@ -189,7 +189,8 @@
(Pretty.str (ext_class c) :: Pretty.str " <" :: Pretty.brk 1 ::
Pretty.breaks (map (Pretty.str o ext_class) cs));
- fun pretty_thms name thms = Pretty.big_list (name ^ ":") (map Display.pretty_thm thms);
+ fun pretty_thms name thms = Pretty.big_list (name ^ ":")
+ (map (Display.pretty_thm_sg sg) thms);
fun pretty_axclass (name, {super_classes, intro, axioms}) = Pretty.block (Pretty.fbreaks
[pretty_class name super_classes, pretty_thms introN [intro], pretty_thms axiomsN axioms]);
--- a/src/Pure/pure_thy.ML Sun Sep 17 22:19:02 2000 +0200
+++ b/src/Pure/pure_thy.ML Sun Sep 17 22:21:31 2000 +0200
@@ -87,7 +87,7 @@
fun pretty sg (ref {space, thms_tab, const_idx = _}) =
let
- val prt_thm = Display.pretty_thm o Thm.transfer_sg sg;
+ val prt_thm = Display.pretty_thm_sg sg;
fun prt_thms (name, [th]) =
Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 1, prt_thm th]
| prt_thms (name, ths) = Pretty.big_list (name ^ ":") (map prt_thm ths);
@@ -213,7 +213,8 @@
fun thms_containing thy consts =
(case filter (is_none o Sign.const_type (Theory.sign_of thy)) consts of
[] => flat (map (containing consts) (thy :: Theory.ancestors_of thy))
- | cs => raise THEORY ("thms_containing: undeclared consts " ^ commas_quote cs, [thy]));
+ | cs => raise THEORY ("thms_containing: undeclared consts " ^ commas_quote cs, [thy]))
+ |> map (apsnd (Thm.transfer thy));