equal
deleted
inserted
replaced
734 |
734 |
735 fun register_alternative_function pred_name mode fun_name = |
735 fun register_alternative_function pred_name mode fun_name = |
736 Alt_Names_Data.map (Symtab.insert_list (op =) (pred_name, (mode, fun_name))) |
736 Alt_Names_Data.map (Symtab.insert_list (op =) (pred_name, (mode, fun_name))) |
737 |
737 |
738 fun alternative_function_of thy pred_name mode = |
738 fun alternative_function_of thy pred_name mode = |
739 AList.lookup (op =) (Symtab.lookup_list (Alt_Names_Data.get thy) pred_name) mode |
739 AList.lookup eq_mode (Symtab.lookup_list (Alt_Names_Data.get thy) pred_name) mode |
740 |
740 |
741 (* datastructures and setup for generic compilation *) |
741 (* datastructures and setup for generic compilation *) |
742 |
742 |
743 datatype compilation_funs = CompilationFuns of { |
743 datatype compilation_funs = CompilationFuns of { |
744 mk_predT : typ -> typ, |
744 mk_predT : typ -> typ, |