# HG changeset patch
# User wenzelm
# Date 969222091 -7200
# Node ID 61eb9f3aa92a5fe58250d8e2abd18fbe32aa7546
# Parent  64bf7da1994aab339551c97aa4f2c8c4e0ce3f85
Display.pretty_thm_sg;

diff -r 64bf7da1994a -r 61eb9f3aa92a src/HOL/Tools/induct_method.ML
--- 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);
diff -r 64bf7da1994a -r 61eb9f3aa92a src/HOL/Tools/inductive_package.ML
--- 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;
 
diff -r 64bf7da1994a -r 61eb9f3aa92a src/HOL/Tools/record_package.ML
--- 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])];
diff -r 64bf7da1994a -r 61eb9f3aa92a src/Pure/Isar/calculation.ML
--- 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);
diff -r 64bf7da1994a -r 61eb9f3aa92a src/Pure/Isar/method.ML
--- 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);
diff -r 64bf7da1994a -r 61eb9f3aa92a src/Pure/axclass.ML
--- 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]);
diff -r 64bf7da1994a -r 61eb9f3aa92a src/Pure/pure_thy.ML
--- 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));