1.1 --- a/src/HOL/Tools/Qelim/cooper_data.ML	Fri Jun 22 10:23:37 2007 +0200
     1.2 +++ b/src/HOL/Tools/Qelim/cooper_data.ML	Fri Jun 22 16:16:23 2007 +0200
     1.3 @@ -48,7 +48,7 @@
     1.4  (
     1.5    type T = simpset * (term list);
     1.6    val empty = (start_ss, allowed_consts);
     1.7 -  fun extend (ss, ts) = (MetaSimplifier.inherit_context empty_ss ss, ts);
     1.8 +  val extend  = I;
     1.9    fun merge _ ((ss1, ts1), (ss2, ts2)) =
    1.10      (merge_ss (ss1, ss2), Library.merge (op aconv) (ts1, ts2));
    1.11  );