1.1 --- a/src/ZF/Tools/inductive_package.ML	Tue Nov 18 18:25:10 2008 +0100
     1.2 +++ b/src/ZF/Tools/inductive_package.ML	Tue Nov 18 18:25:42 2008 +0100
     1.3 @@ -262,7 +262,7 @@
     1.4                  ORELSE' bound_hyp_subst_tac))
     1.5        THEN prune_params_tac
     1.6            (*Mutual recursion: collapse references to Part(D,h)*)
     1.7 -      THEN fold_tac part_rec_defs;
     1.8 +      THEN (PRIMITIVE (fold_rule part_rec_defs));
     1.9  
    1.10    (*Elimination*)
    1.11    val elim = rule_by_tactic basic_elim_tac