src/Provers/simplifier.ML
changeset 406 4d4e0442b106
parent 217 c972c57e7762
child 433 1e4f420523ae
--- 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();