--- a/src/ZF/ind_syntax.ML Thu Mar 19 17:25:57 2015 +0100
+++ b/src/ZF/ind_syntax.ML Thu Mar 19 22:30:57 2015 +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 =
- Rule_Insts.read_instantiate @{context} [(("W", 0), "Q")] ["Q"]
+ Rule_Insts.read_instantiate @{context} [((("W", 0), Position.none), "Q")] ["Q"]
(make_elim (@{thm equalityD1} RS @{thm subsetD} RS @{thm CollectD2}));