src/HOL/Relation.ML
changeset 1786 8a31d85d27b8
parent 1761 29e08d527ba1
child 1842 a9c36056d320
     1.1 --- a/src/HOL/Relation.ML	Mon Jun 03 11:44:44 1996 +0200
     1.2 +++ b/src/HOL/Relation.ML	Mon Jun 03 17:10:56 1996 +0200
     1.3 @@ -162,7 +162,7 @@
     1.4      "[| b: r^^A;  !!x.[| (x,b): r;  x:A |] ==> P |] ==> P"
     1.5   (fn major::prems=>
     1.6    [ (rtac (major RS CollectE) 1),
     1.7 -    (safe_tac set_cs),
     1.8 +    (safe_tac (!claset)),
     1.9      (etac RangeE 1),
    1.10      (rtac (hd prems) 1),
    1.11      (REPEAT (etac bexE 1 ORELSE ares_tac prems 1)) ]);