src/ZF/ind_syntax.ML

--- a/src/ZF/ind_syntax.ML	Wed Jun 11 18:01:36 2008 +0200
+++ b/src/ZF/ind_syntax.ML	Wed Jun 11 18:02:00 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 =
-    read_instantiate [("W","?Q")]
+    Drule.read_instantiate [("W","?Q")]
         (make_elim (@{thm equalityD1} RS @{thm subsetD} RS @{thm CollectD2}));