# HG changeset patch # User krauss # Date 1154536426 -7200 # Node ID 23f5cd23c1e1541b72e673d8c6c20427c424bd0c # Parent a17c737c82dfc7b4b49ccef1c6efcf24f8f3a63a Added type constraint to please sml/nj diff -r a17c737c82df -r 23f5cd23c1e1 src/HOL/Tools/function_package/fundef_package.ML --- a/src/HOL/Tools/function_package/fundef_package.ML Wed Aug 02 18:30:57 2006 +0200 +++ b/src/HOL/Tools/function_package/fundef_package.ML Wed Aug 02 18:33:46 2006 +0200 @@ -76,7 +76,7 @@ add_fundef_data name (fundef_data, mutual_info, spec) thy end -fun gen_add_fundef prep_att eqns_attss preprocess thy = +fun gen_add_fundef prep_att eqns_attss (preprocess : bool) thy = let fun prep_eqns neqs = neqs