src/ZF/Tools/inductive_package.ML

--- a/src/ZF/Tools/inductive_package.ML	Wed Jun 29 18:12:34 2011 +0200
+++ b/src/ZF/Tools/inductive_package.ML	Wed Jun 29 20:39:41 2011 +0200
@@ -329,7 +329,7 @@
      val min_ss = Simplifier.global_context thy empty_ss
            setmksimps (K (map mk_eq o ZF_atomize o gen_all))
            setSolver (mk_solver "minimal"
-                      (fn prems => resolve_tac (triv_rls@prems)
+                      (fn ss => resolve_tac (triv_rls @ prems_of_ss ss)
                                    ORELSE' assume_tac
                                    ORELSE' etac @{thm FalseE}));