merge is now identity

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