# HG changeset patch
# User wenzelm
# Date 997996752 -7200
# Node ID e80a712982e1086fdae0b61d5cd5ffa20f8a020b
# Parent  3b6415035d1a419f6d526368ab6f66acc13b0886
prefer immediate monos;
tuned;

diff -r 3b6415035d1a -r e80a712982e1 src/HOL/Tools/inductive_package.ML
--- a/src/HOL/Tools/inductive_package.ML	Wed Aug 15 22:20:30 2001 +0200
+++ b/src/HOL/Tools/inductive_package.ML	Thu Aug 16 23:19:12 2001 +0200
@@ -100,8 +100,8 @@
   val empty = (Symtab.empty, []);
   val copy = I;
   val prep_ext = I;
-  fun merge ((tab1, monos1), (tab2, monos2)) = (Symtab.merge (K true) (tab1, tab2),
-    Library.generic_merge Thm.eq_thm I I monos1 monos2);
+  fun merge ((tab1, monos1), (tab2, monos2)) =
+    (Symtab.merge (K true) (tab1, tab2), Drule.merge_rules (monos1, monos2));
 
   fun print sg (tab, monos) =
     [Pretty.strs ("(co)inductives:" :: map #1 (Sign.cond_extern_table sg Sign.constK tab)),
@@ -480,7 +480,7 @@
   Goals.prove_goalw_cterm []      (*NO SkipProof.prove_goalw_cterm here!*)
     (Thm.cterm_of (Theory.sign_of thy) (HOLogic.mk_Trueprop
       (Const (mono_name, (setT --> setT) --> HOLogic.boolT) $ fp_fun)))
-    (fn _ => [rtac monoI 1, REPEAT (ares_tac (get_monos thy @ flat (map mk_mono monos)) 1)]));
+    (fn _ => [rtac monoI 1, REPEAT (ares_tac (flat (map mk_mono monos) @ get_monos thy) 1)]));
 
 
 (* prove introduction rules *)