src/ZF/Tools/inductive_package.ML
changeset 28839 32d498cf7595
parent 28678 d93980a6c3cb
child 28965 1de908189869
--- a/src/ZF/Tools/inductive_package.ML	Tue Nov 18 18:25:10 2008 +0100
+++ b/src/ZF/Tools/inductive_package.ML	Tue Nov 18 18:25:42 2008 +0100
@@ -262,7 +262,7 @@
                 ORELSE' bound_hyp_subst_tac))
       THEN prune_params_tac
           (*Mutual recursion: collapse references to Part(D,h)*)
-      THEN fold_tac part_rec_defs;
+      THEN (PRIMITIVE (fold_rule part_rec_defs));
 
   (*Elimination*)
   val elim = rule_by_tactic basic_elim_tac