src/HOL/Tools/simpdata.ML
changeset 42460 1805c67dc7aa
parent 42458 5dfae6d348fd
child 42478 8a526c010c3b
     1.1 --- a/src/HOL/Tools/simpdata.ML	Fri Apr 22 15:05:04 2011 +0200
     1.2 +++ b/src/HOL/Tools/simpdata.ML	Fri Apr 22 15:24:00 2011 +0200
     1.3 @@ -10,11 +10,11 @@
     1.4  structure Quantifier1 = Quantifier1
     1.5  (
     1.6    (*abstract syntax*)
     1.7 -  fun dest_eq ((c as Const(@{const_name HOL.eq},_)) $ s $ t) = SOME (c, s, t)
     1.8 +  fun dest_eq (Const(@{const_name HOL.eq},_) $ s $ t) = SOME (s, t)
     1.9      | dest_eq _ = NONE;
    1.10 -  fun dest_conj ((c as Const(@{const_name HOL.conj},_)) $ s $ t) = SOME (c, s, t)
    1.11 +  fun dest_conj (Const(@{const_name HOL.conj},_) $ s $ t) = SOME (s, t)
    1.12      | dest_conj _ = NONE;
    1.13 -  fun dest_imp ((c as Const(@{const_name HOL.implies},_)) $ s $ t) = SOME (c, s, t)
    1.14 +  fun dest_imp (Const(@{const_name HOL.implies},_) $ s $ t) = SOME (s, t)
    1.15      | dest_imp _ = NONE;
    1.16    val conj = HOLogic.conj
    1.17    val imp  = HOLogic.imp