equal
deleted
inserted
replaced
392 else error ("primrec_new error:\n " ^ str ^ "\nin\n " ^ |
392 else error ("primrec_new error:\n " ^ str ^ "\nin\n " ^ |
393 space_implode "\n " (map (quote o Syntax.string_of_term lthy) eqns)); |
393 space_implode "\n " (map (quote o Syntax.string_of_term lthy) eqns)); |
394 |
394 |
395 local |
395 local |
396 |
396 |
397 fun gen_primrec prep_spec raw_fixes raw_spec lthy = |
397 fun gen_primrec prep_spec (raw_fixes : (binding * 'a option * mixfix) list) raw_spec lthy = |
398 let |
398 let |
399 val d = duplicates (op =) (map (Binding.name_of o #1) raw_fixes) |
399 val d = duplicates (op =) (map (Binding.name_of o #1) raw_fixes) |
400 val _ = null d orelse primrec_error ("duplicate function name(s): " ^ commas d); |
400 val _ = null d orelse primrec_error ("duplicate function name(s): " ^ commas d); |
401 |
401 |
402 val (fixes, specs) = fst (prep_spec raw_fixes raw_spec lthy); |
402 val (fixes, specs) = fst (prep_spec raw_fixes raw_spec lthy); |