prefer immediate monos;
authorwenzelm
Thu Aug 16 23:19:12 2001 +0200 (2001-08-16 ago)
changeset 11502e80a712982e1
parent 11501 3b6415035d1a
child 11503 4c25eef6f325
prefer immediate monos;
tuned;
src/HOL/Tools/inductive_package.ML
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Wed Aug 15 22:20:30 2001 +0200
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Thu Aug 16 23:19:12 2001 +0200
     1.3 @@ -100,8 +100,8 @@
     1.4    val empty = (Symtab.empty, []);
     1.5    val copy = I;
     1.6    val prep_ext = I;
     1.7 -  fun merge ((tab1, monos1), (tab2, monos2)) = (Symtab.merge (K true) (tab1, tab2),
     1.8 -    Library.generic_merge Thm.eq_thm I I monos1 monos2);
     1.9 +  fun merge ((tab1, monos1), (tab2, monos2)) =
    1.10 +    (Symtab.merge (K true) (tab1, tab2), Drule.merge_rules (monos1, monos2));
    1.11  
    1.12    fun print sg (tab, monos) =
    1.13      [Pretty.strs ("(co)inductives:" :: map #1 (Sign.cond_extern_table sg Sign.constK tab)),
    1.14 @@ -480,7 +480,7 @@
    1.15    Goals.prove_goalw_cterm []      (*NO SkipProof.prove_goalw_cterm here!*)
    1.16      (Thm.cterm_of (Theory.sign_of thy) (HOLogic.mk_Trueprop
    1.17        (Const (mono_name, (setT --> setT) --> HOLogic.boolT) $ fp_fun)))
    1.18 -    (fn _ => [rtac monoI 1, REPEAT (ares_tac (get_monos thy @ flat (map mk_mono monos)) 1)]));
    1.19 +    (fn _ => [rtac monoI 1, REPEAT (ares_tac (flat (map mk_mono monos) @ get_monos thy) 1)]));
    1.20  
    1.21  
    1.22  (* prove introduction rules *)