# HG changeset patch
# User wenzelm
# Date 891685747 -7200
# Node ID 9db0916ecdae8fef93396f0a8255f0b9b26bb82e
# Parent  03fd006fb97ba6889ae838bab64143c16e3fced2
no open Simplifier;

diff -r 03fd006fb97b -r 9db0916ecdae src/FOL/simpdata.ML
--- a/src/FOL/simpdata.ML	Sat Apr 04 12:28:39 1998 +0200
+++ b/src/FOL/simpdata.ML	Sat Apr 04 12:29:07 1998 +0200
@@ -188,8 +188,6 @@
   (fn [prem] => [rewtac prem, rtac refl 1]);
 
 
-open Simplifier;
-
 (** make simplification procedures for quantifier elimination **)
 structure Quantifier1 = Quantifier1Fun(
 struct
diff -r 03fd006fb97b -r 9db0916ecdae src/HOL/simpdata.ML
--- a/src/HOL/simpdata.ML	Sat Apr 04 12:28:39 1998 +0200
+++ b/src/HOL/simpdata.ML	Sat Apr 04 12:29:07 1998 +0200
@@ -3,13 +3,11 @@
     Author:     Tobias Nipkow
     Copyright   1991  University of Cambridge
 
-Instantiation of the generic simplifier
+Instantiation of the generic simplifier.
 *)
 
 section "Simplifier";
 
-open Simplifier;
-
 (*** Addition of rules to simpsets and clasets simultaneously ***)
 
 (*Takes UNCONDITIONAL theorems of the form A<->B to 
@@ -450,9 +448,6 @@
 
 
 
-
-
-
 (*** Integration of simplifier with classical reasoner ***)
 
 (* rot_eq_tac rotates the first equality premise of subgoal i to the front,