src/Pure/simplifier.ML
changeset 21708 45e7491bea47
parent 21687 f689f729afab
child 22095 07875394618e
--- a/src/Pure/simplifier.ML	Thu Dec 07 21:44:13 2006 +0100
+++ b/src/Pure/simplifier.ML	Thu Dec 07 23:16:55 2006 +0100
@@ -80,6 +80,9 @@
 structure Simplifier: SIMPLIFIER =
 struct
 
+open MetaSimplifier;
+
+
 (** simpset data **)
 
 (* global simpsets *)
@@ -348,9 +351,6 @@
     thy
   end);
 
-
-open MetaSimplifier;
-
 end;
 
 structure BasicSimplifier: BASIC_SIMPLIFIER = Simplifier;