1.1 --- a/src/ZF/indrule.ML	Tue Jul 16 15:48:27 1996 +0200
     1.2 +++ b/src/ZF/indrule.ML	Tue Jul 16 15:49:46 1996 +0200
     1.3 @@ -72,6 +72,20 @@
     1.4  val ind_prems = map (induct_prem (map (rpair pred) Inductive.rec_tms)) 
     1.5                      Inductive.intr_tms;
     1.6  
     1.7 +(*Debugging code...
     1.8 +val _ = writeln "ind_prems = ";
     1.9 +val _ = seq (writeln o Sign.string_of_term sign) ind_prems;
    1.10 +*)
    1.11 +
    1.12 +(*We use a MINIMAL simpset because others (such as FOL_ss) contain too many
    1.13 +  simplifications.  If the premises get simplified, then the proofs will 
    1.14 +  fail.  *)
    1.15 +val min_ss = empty_ss
    1.16 +      setmksimps (map mk_meta_eq o ZF_atomize o gen_all)
    1.17 +      setsolver  (fn prems => resolve_tac (triv_rls@prems) 
    1.18 +			      ORELSE' assume_tac
    1.19 +			      ORELSE' etac FalseE);
    1.20 +
    1.21  val quant_induct = 
    1.22      prove_goalw_cterm part_rec_defs 
    1.23        (cterm_of sign 
    1.24 @@ -81,7 +95,7 @@
    1.25         [rtac (impI RS allI) 1,
    1.26          DETERM (etac Intr_elim.raw_induct 1),
    1.27          (*Push Part inside Collect*)
    1.28 -        asm_full_simp_tac (FOL_ss addsimps [Part_Collect]) 1,
    1.29 +        full_simp_tac (min_ss addsimps [Part_Collect]) 1,
    1.30          REPEAT (FIRSTGOAL (eresolve_tac [CollectE, exE, conjE, disjE] ORELSE'
    1.31                             hyp_subst_tac)),
    1.32          ind_tac (rev prems) (length prems) ]);
    1.33 @@ -150,7 +164,7 @@
    1.34  (*Simplification largely reduces the mutual induction rule to the 
    1.35    standard rule*)
    1.36  val mut_ss = 
    1.37 -    FOL_ss addsimps   [Su.distinct, Su.distinct', Su.inl_iff, Su.inr_iff];
    1.38 +    min_ss addsimps [Su.distinct, Su.distinct', Su.inl_iff, Su.inr_iff];
    1.39  
    1.40  val all_defs = Inductive.con_defs @ part_rec_defs;
    1.41  
    1.42 @@ -174,8 +188,11 @@
    1.43             rewrite_goals_tac all_defs  THEN
    1.44             simp_tac (mut_ss addsimps [Part_iff]) 1  THEN
    1.45             IF_UNSOLVED (*simp_tac may have finished it off!*)
    1.46 -             ((*simplify assumptions, but don't accept new rewrite rules!*)
    1.47 -              asm_full_simp_tac (mut_ss setmksimps (fn _=>[])) 1  THEN
    1.48 +             ((*simplify assumptions*)
    1.49 +              (*some risk of excessive simplification here -- might have
    1.50 +	        to identify the bare minimum set of rewrites*)
    1.51 +              full_simp_tac 
    1.52 +	         (mut_ss addsimps (conj_rews @ imp_rews @ quant_rews)) 1  THEN
    1.53                (*unpackage and use "prem" in the corresponding place*)
    1.54                REPEAT (rtac impI 1)  THEN
    1.55                rtac (rewrite_rule all_defs prem) 1  THEN