src/FOL/simpdata.ML
changeset 42458 5dfae6d348fd
parent 42455 6702c984bf5a
child 42460 1805c67dc7aa
     1.1 --- a/src/FOL/simpdata.ML	Fri Apr 22 14:38:49 2011 +0200
     1.2 +++ b/src/FOL/simpdata.ML	Fri Apr 22 14:53:11 2011 +0200
     1.3 @@ -52,8 +52,8 @@
     1.4  
     1.5  
     1.6  (** make simplification procedures for quantifier elimination **)
     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 eq},_)) $ s $ t) = SOME(c,s,t)
    1.13      | dest_eq _ = NONE;
    1.14 @@ -78,7 +78,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  
    1.22  (*** Case splitting ***)