src/ZF/ind_syntax.ML
changeset 27153 56b6cdce22f1
parent 26939 1035c89b4c02
child 27230 c0103bc7f7eb
     1.1 --- a/src/ZF/ind_syntax.ML	Wed Jun 11 18:01:36 2008 +0200
     1.2 +++ b/src/ZF/ind_syntax.ML	Wed Jun 11 18:02:00 2008 +0200
     1.3 @@ -51,7 +51,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 [("W","?Q")]
     1.8 +    Drule.read_instantiate [("W","?Q")]
     1.9          (make_elim (@{thm equalityD1} RS @{thm subsetD} RS @{thm CollectD2}));
    1.10  
    1.11