author | traytel |
Wed, 02 Oct 2013 15:13:41 +0200 | |
changeset 54028 | 4d087a8950f3 |
parent 54027 | e5853a648b59 |
child 54029 | 4edfd0fd5536 |
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML Wed Oct 02 13:29:04 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML Wed Oct 02 15:13:41 2013 +0200 @@ -394,7 +394,7 @@ local -fun gen_primrec prep_spec raw_fixes raw_spec lthy = +fun gen_primrec prep_spec (raw_fixes : (binding * 'a option * mixfix) list) raw_spec lthy = let val d = duplicates (op =) (map (Binding.name_of o #1) raw_fixes) val _ = null d orelse primrec_error ("duplicate function name(s): " ^ commas d);