equal
deleted
inserted
replaced
677 else (); |
677 else (); |
678 val _ = if (is_some o get_datatype_of_constr thy) c |
678 val _ = if (is_some o get_datatype_of_constr thy) c |
679 then error ("Rejected equation for datatype constructor:\n" |
679 then error ("Rejected equation for datatype constructor:\n" |
680 ^ string_of_thm func) |
680 ^ string_of_thm func) |
681 else (); |
681 else (); |
682 in map_exec_purge (SOME [c]) (map_funcs |
682 in |
683 (Symtab.map_default |
683 (map_exec_purge (SOME [c]) o map_funcs) (Symtab.map_default |
684 (c, (Susp.value [], [])) (add_thm func))) thy |
684 (c, (Susp.value [], [])) (add_thm func)) thy |
685 end |
685 end |
686 | add_func false thm thy = |
686 | add_func false thm thy = |
687 case mk_func_liberal thm |
687 case mk_func_liberal thm |
688 of SOME func => let |
688 of SOME func => let |
689 val c = const_of_func thy func |
689 val c = const_of_func thy func |