| changeset 35408 | b48ab741683b |
| parent 35232 | f588e1169c8b |
| child 35845 | e5980f0ad025 |
--- a/src/Pure/meta_simplifier.ML Sat Feb 27 22:52:25 2010 +0100 +++ b/src/Pure/meta_simplifier.ML Sat Feb 27 23:13:01 2010 +0100 @@ -755,7 +755,7 @@ mk_eq_True = K NONE, reorient = default_reorient}; -val empty_ss = init_ss basic_mk_rews TermOrd.termless (K (K no_tac)) ([], []); +val empty_ss = init_ss basic_mk_rews Term_Ord.termless (K (K no_tac)) ([], []); (* merge *) (*NOTE: ignores some fields of 2nd simpset*)