src/ZF/ind_syntax.ML

--- a/src/ZF/ind_syntax.ML	Mon Jun 16 17:54:42 2008 +0200
+++ b/src/ZF/ind_syntax.ML	Mon Jun 16 17:54:43 2008 +0200
@@ -51,7 +51,7 @@
 (*For deriving cases rules.  CollectD2 discards the domain, which is redundant;
   read_instantiate replaces a propositional variable by a formula variable*)
 val equals_CollectD =
-    Drule.read_instantiate [("W","?Q")]
+    RuleInsts.read_instantiate @{context} [(("W", 0), "?Q")]
         (make_elim (@{thm equalityD1} RS @{thm subsetD} RS @{thm CollectD2}));