equal
deleted
inserted
replaced
1585 val dups = duplicates (op =) (map (Binding.name_of o #1) raw_fixes); |
1585 val dups = duplicates (op =) (map (Binding.name_of o #1) raw_fixes); |
1586 val _ = null dups orelse error ("Duplicate function name " ^ quote (hd dups)); |
1586 val _ = null dups orelse error ("Duplicate function name " ^ quote (hd dups)); |
1587 |
1587 |
1588 val (raw_specs, of_specs_opt) = |
1588 val (raw_specs, of_specs_opt) = |
1589 split_list raw_specs_of ||> map (Option.map (Syntax.read_term lthy)); |
1589 split_list raw_specs_of ||> map (Option.map (Syntax.read_term lthy)); |
1590 val (fixes, specs) = fst (Specification.read_spec raw_fixes raw_specs lthy); |
1590 val (fixes, specs) = |
|
1591 fst (Specification.read_multi_specs raw_fixes (map (rpair []) raw_specs) lthy); |
1591 in |
1592 in |
1592 primcorec_ursive auto opts fixes specs of_specs_opt lthy |
1593 primcorec_ursive auto opts fixes specs of_specs_opt lthy |
1593 end; |
1594 end; |
1594 |
1595 |
1595 val primcorecursive_cmd = (fn (goalss, after_qed, lthy) => |
1596 val primcorecursive_cmd = (fn (goalss, after_qed, lthy) => |