# HG changeset patch
# User chaieb
# Date 1182521783 -7200
# Node ID 688987d0bab484e45b4a3fc17c0809159043aeb1
# Parent  997bca36d4fee77e3004cd8953ae2b1ffafba20d
merge is now identity

diff -r 997bca36d4fe -r 688987d0bab4 src/HOL/Tools/Qelim/cooper_data.ML
--- 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));
 );