simpset is hidden in a functor now.
authornipkow
Tue, 31 May 1994 13:17:41 +0200
changeset 406 4d4e0442b106
parent 405 c97514f63633
child 407 8039ac1065f7
simpset is hidden in a functor now.
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();