changeset 55151 | f331472f1027 |
parent 55143 | 04448228381d |
child 59755 | f8d164ab0dc1 |
--- 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}));