tuned;
authorwenzelm
Fri Dec 17 13:12:58 2010 +0100 (2010-12-17)
changeset 412248a104c2a186f
parent 41223 cf5e008d38c4
child 41225 bd4ecd48c21f
tuned;
src/HOL/Tools/SMT/smt_normalize.ML
src/HOL/Tools/SMT/smt_translate.ML
     1.1 --- a/src/HOL/Tools/SMT/smt_normalize.ML	Fri Dec 17 08:37:35 2010 +0100
     1.2 +++ b/src/HOL/Tools/SMT/smt_normalize.ML	Fri Dec 17 13:12:58 2010 +0100
     1.3 @@ -589,7 +589,7 @@
     1.4    type T = extra_norm U.dict
     1.5    val empty = []
     1.6    val extend = I
     1.7 -  fun merge xx = U.dict_merge fst xx
     1.8 +  fun merge data = U.dict_merge fst data
     1.9  )
    1.10  
    1.11  fun add_extra_norm (cs, norm) = Extra_Norms.map (U.dict_update (cs, norm))
     2.1 --- a/src/HOL/Tools/SMT/smt_translate.ML	Fri Dec 17 08:37:35 2010 +0100
     2.2 +++ b/src/HOL/Tools/SMT/smt_translate.ML	Fri Dec 17 13:12:58 2010 +0100
     2.3 @@ -588,7 +588,7 @@
     2.4    type T = (Proof.context -> config) U.dict
     2.5    val empty = []
     2.6    val extend = I
     2.7 -  fun merge xx = U.dict_merge fst xx
     2.8 +  fun merge data = U.dict_merge fst data
     2.9  )
    2.10  
    2.11  fun add_config (cs, cfg) = Configs.map (U.dict_update (cs, cfg))