src/HOL/Tools/SMT/smt_normalize.ML
changeset 41193 dc33b8ea4526
parent 41126 e0bd443c0fdd
child 41194 9796e5e01b61
     1.1 --- a/src/HOL/Tools/SMT/smt_normalize.ML	Wed Dec 15 17:14:44 2010 +0100
     1.2 +++ b/src/HOL/Tools/SMT/smt_normalize.ML	Thu Dec 16 12:05:00 2010 +0000
     1.3 @@ -586,7 +586,7 @@
     1.4    type T = extra_norm U.dict
     1.5    val empty = []
     1.6    val extend = I
     1.7 -  val merge = U.dict_merge fst
     1.8 +  fun merge xx = U.dict_merge fst xx
     1.9  )
    1.10  
    1.11  fun add_extra_norm (cs, norm) = Extra_Norms.map (U.dict_update (cs, norm))