src/ZF/ind_syntax.ML
changeset 55151 f331472f1027
parent 55143 04448228381d
child 59755 f8d164ab0dc1
     1.1 --- a/src/ZF/ind_syntax.ML	Sat Jan 25 23:50:49 2014 +0100
     1.2 +++ b/src/ZF/ind_syntax.ML	Sun Jan 26 13:45:40 2014 +0100
     1.3 @@ -50,7 +50,7 @@
     1.4  (*For deriving cases rules.  CollectD2 discards the domain, which is redundant;
     1.5    read_instantiate replaces a propositional variable by a formula variable*)
     1.6  val equals_CollectD =
     1.7 -    read_instantiate @{context} [(("W", 0), "Q")] ["Q"]
     1.8 +    Rule_Insts.read_instantiate @{context} [(("W", 0), "Q")] ["Q"]
     1.9          (make_elim (@{thm equalityD1} RS @{thm subsetD} RS @{thm CollectD2}));
    1.10  
    1.11