--- 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))
--- 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))