# 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