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;