# 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 *)