made SML/NJ happy
authortraytel
Wed Oct 02 15:13:41 2013 +0200 (2013-10-02)
changeset 540284d087a8950f3
parent 54027 e5853a648b59
child 54029 4edfd0fd5536
made SML/NJ happy
src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML
     1.1 --- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Wed Oct 02 13:29:04 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Wed Oct 02 15:13:41 2013 +0200
     1.3 @@ -394,7 +394,7 @@
     1.4  
     1.5  local
     1.6  
     1.7 -fun gen_primrec prep_spec raw_fixes raw_spec lthy =
     1.8 +fun gen_primrec prep_spec (raw_fixes : (binding * 'a option * mixfix) list) raw_spec lthy =
     1.9    let
    1.10      val d = duplicates (op =) (map (Binding.name_of o #1) raw_fixes)
    1.11      val _ = null d orelse primrec_error ("duplicate function name(s): " ^ commas d);