author | haftmann |
Fri, 19 Nov 2010 10:37:06 +0100 | |
changeset 40614 | d6eeffa0d9a0 |
parent 40613 | 23626b388e07 |
child 40615 | ab551d108feb |
--- a/src/HOL/Tools/functorial_mappers.ML Fri Nov 19 10:04:08 2010 +0100 +++ b/src/HOL/Tools/functorial_mappers.ML Fri Nov 19 10:37:06 2010 +0100 @@ -30,7 +30,7 @@ structure Data = Theory_Data( type T = entry Symtab.table val empty = Symtab.empty - val merge = Symtab.merge (K true) + fun merge (xy : T * T) = Symtab.merge (K true) xy val extend = I );