equal
deleted
inserted
replaced
885 let |
885 let |
886 fun declare_sym decl decls = |
886 fun declare_sym decl decls = |
887 case type_sys of |
887 case type_sys of |
888 Preds (Polymorphic, All_Types) => insert_type #3 decl decls |
888 Preds (Polymorphic, All_Types) => insert_type #3 decl decls |
889 | _ => insert (op =) decl decls |
889 | _ => insert (op =) decl decls |
890 fun do_term tm = |
890 and do_term tm = |
891 let val (head, args) = strip_combterm_comb tm in |
891 let val (head, args) = strip_combterm_comb tm in |
892 (case head of |
892 (case head of |
893 CombConst ((s, s'), T, T_args) => |
893 CombConst ((s, s'), T, T_args) => |
894 let val pred_sym = is_pred_sym repaired_sym_tab s in |
894 let val pred_sym = is_pred_sym repaired_sym_tab s in |
895 if should_declare_sym type_sys pred_sym s then |
895 if should_declare_sym type_sys pred_sym s then |