src/HOL/Tools/simpdata.ML
changeset 42458 5dfae6d348fd
parent 42455 6702c984bf5a
child 42460 1805c67dc7aa
     1.1 --- a/src/HOL/Tools/simpdata.ML	Fri Apr 22 14:38:49 2011 +0200
     1.2 +++ b/src/HOL/Tools/simpdata.ML	Fri Apr 22 14:53:11 2011 +0200
     1.3 @@ -7,8 +7,8 @@
     1.4  
     1.5  (** tools setup **)
     1.6  
     1.7 -structure Quantifier1 = Quantifier1Fun
     1.8 -(struct
     1.9 +structure Quantifier1 = Quantifier1
    1.10 +(
    1.11    (*abstract syntax*)
    1.12    fun dest_eq ((c as Const(@{const_name HOL.eq},_)) $ s $ t) = SOME (c, s, t)
    1.13      | dest_eq _ = NONE;
    1.14 @@ -33,7 +33,7 @@
    1.15    val iff_exI = @{thm iff_exI}
    1.16    val all_comm = @{thm all_comm}
    1.17    val ex_comm = @{thm ex_comm}
    1.18 -end);
    1.19 +);
    1.20  
    1.21  structure Simpdata =
    1.22  struct