# HG changeset patch
# User wenzelm
# Date 1292587978 -3600
# Node ID 8a104c2a186f394f85d0acd4c822967c73498e7d
# Parent  cf5e008d38c425531b2c4319985d6e915e20b067
tuned;

diff -r cf5e008d38c4 -r 8a104c2a186f src/HOL/Tools/SMT/smt_normalize.ML
--- a/src/HOL/Tools/SMT/smt_normalize.ML	Fri Dec 17 08:37:35 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_normalize.ML	Fri Dec 17 13:12:58 2010 +0100
@@ -589,7 +589,7 @@
   type T = extra_norm U.dict
   val empty = []
   val extend = I
-  fun merge xx = U.dict_merge fst xx
+  fun merge data = U.dict_merge fst data
 )
 
 fun add_extra_norm (cs, norm) = Extra_Norms.map (U.dict_update (cs, norm))
diff -r cf5e008d38c4 -r 8a104c2a186f src/HOL/Tools/SMT/smt_translate.ML
--- a/src/HOL/Tools/SMT/smt_translate.ML	Fri Dec 17 08:37:35 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_translate.ML	Fri Dec 17 13:12:58 2010 +0100
@@ -588,7 +588,7 @@
   type T = (Proof.context -> config) U.dict
   val empty = []
   val extend = I
-  fun merge xx = U.dict_merge fst xx
+  fun merge data = U.dict_merge fst data
 )
 
 fun add_config (cs, cfg) = Configs.map (U.dict_update (cs, cfg))