src/Pure/meta_simplifier.ML
changeset 29269 5c25a2012975
parent 28839 32d498cf7595
child 30318 3d03190d2864
     1.1 --- a/src/Pure/meta_simplifier.ML	Wed Dec 31 00:08:14 2008 +0100
     1.2 +++ b/src/Pure/meta_simplifier.ML	Wed Dec 31 15:30:10 2008 +0100
     1.3 @@ -1,6 +1,5 @@
     1.4  (*  Title:      Pure/meta_simplifier.ML
     1.5 -    ID:         $Id$
     1.6 -    Author:     Tobias Nipkow and Stefan Berghofer
     1.7 +    Author:     Tobias Nipkow and Stefan Berghofer, TU Muenchen
     1.8  
     1.9  Meta-level Simplification.
    1.10  *)
    1.11 @@ -788,7 +787,7 @@
    1.12    mk_eq_True = K NONE,
    1.13    reorient = default_reorient};
    1.14  
    1.15 -val empty_ss = init_ss basic_mk_rews Term.termless (K (K no_tac)) ([], []);
    1.16 +val empty_ss = init_ss basic_mk_rews TermOrd.termless (K (K no_tac)) ([], []);
    1.17  
    1.18  
    1.19  (* merge *)  (*NOTE: ignores some fields of 2nd simpset*)