diff -r 0940309ed8f1 -r f331472f1027 src/ZF/ind_syntax.ML
--- a/src/ZF/ind_syntax.ML	Sat Jan 25 23:50:49 2014 +0100
+++ b/src/ZF/ind_syntax.ML	Sun Jan 26 13:45:40 2014 +0100
@@ -50,7 +50,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 @{context} [(("W", 0), "Q")] ["Q"]
+    Rule_Insts.read_instantiate @{context} [(("W", 0), "Q")] ["Q"]
         (make_elim (@{thm equalityD1} RS @{thm subsetD} RS @{thm CollectD2}));