author | wenzelm |
Sat, 02 Jun 2007 18:35:38 +0200 | |
changeset 23206 | 209e32e7c91e |
parent 23205 | b12f1c03cc9a |
child 23207 | 769f7762f531 |
--- a/src/HOL/Tools/function_package/fundef_common.ML Sat Jun 02 18:05:34 2007 +0200 +++ b/src/HOL/Tools/function_package/fundef_common.ML Sat Jun 02 18:35:38 2007 +0200 @@ -276,7 +276,7 @@ structure Preprocessor = GenericDataFun ( type T = preproc - val empty = empty_preproc check_defs + val empty : T = empty_preproc check_defs val extend = I fun merge _ (a, _) = a );