src/Pure/simplifier.ML
changeset 21708 45e7491bea47
parent 21687 f689f729afab
child 22095 07875394618e
     1.1 --- a/src/Pure/simplifier.ML	Thu Dec 07 21:44:13 2006 +0100
     1.2 +++ b/src/Pure/simplifier.ML	Thu Dec 07 23:16:55 2006 +0100
     1.3 @@ -80,6 +80,9 @@
     1.4  structure Simplifier: SIMPLIFIER =
     1.5  struct
     1.6  
     1.7 +open MetaSimplifier;
     1.8 +
     1.9 +
    1.10  (** simpset data **)
    1.11  
    1.12  (* global simpsets *)
    1.13 @@ -348,9 +351,6 @@
    1.14      thy
    1.15    end);
    1.16  
    1.17 -
    1.18 -open MetaSimplifier;
    1.19 -
    1.20  end;
    1.21  
    1.22  structure BasicSimplifier: BASIC_SIMPLIFIER = Simplifier;