# HG changeset patch
# User nipkow
# Date 770383061 -7200
# Node ID 4d4e0442b106490a3a0195e20cd6a4fb8bf9ce2d
# Parent  c97514f63633cd18944fd57aa343d1fa1f9e326e
simpset is hidden in a functor now.

diff -r c97514f63633 -r 4d4e0442b106 src/Provers/simplifier.ML
--- a/src/Provers/simplifier.ML	Sun May 29 15:14:28 1994 +0200
+++ b/src/Provers/simplifier.ML	Tue May 31 13:17:41 1994 +0200
@@ -28,7 +28,7 @@
   val simp_tac: simpset -> int -> tactic
 end;
 
-structure Simplifier:SIMPLIFIER =
+functor SimplifierFUN():SIMPLIFIER =
 struct
 
 datatype simpset =
@@ -157,3 +157,5 @@
 val simp_tac = gen_simp_tac (false,false);
 
 end;
+
+structure Simplifier = SimplifierFUN();