src/FOL/simpdata.ML
changeset 4794 9db0916ecdae
parent 4669 06f3c56dcba8
child 4930 89271bc4e7ed
     1.1 --- a/src/FOL/simpdata.ML	Sat Apr 04 12:28:39 1998 +0200
     1.2 +++ b/src/FOL/simpdata.ML	Sat Apr 04 12:29:07 1998 +0200
     1.3 @@ -188,8 +188,6 @@
     1.4    (fn [prem] => [rewtac prem, rtac refl 1]);
     1.5  
     1.6  
     1.7 -open Simplifier;
     1.8 -
     1.9  (** make simplification procedures for quantifier elimination **)
    1.10  structure Quantifier1 = Quantifier1Fun(
    1.11  struct