src/ZF/ind_syntax.ML

--- a/src/ZF/ind_syntax.ML	Sun Oct 07 15:49:25 2007 +0200
+++ b/src/ZF/ind_syntax.ML	Sun Oct 07 21:19:31 2007 +0200
@@ -64,7 +64,7 @@
   read_instantiate replaces a propositional variable by a formula variable*)
 val equals_CollectD = 
     read_instantiate [("W","?Q")]
-        (make_elim (equalityD1 RS subsetD RS CollectD2));
+        (make_elim (@{thm equalityD1} RS @{thm subsetD} RS @{thm CollectD2}));
 
 
 (** For datatype definitions **)