170 fun merge _ |
170 fun merge _ |
171 ({to_set_simps = to_set_simps1, to_pred_simps = to_pred_simps1, |
171 ({to_set_simps = to_set_simps1, to_pred_simps = to_pred_simps1, |
172 set_arities = set_arities1, pred_arities = pred_arities1}, |
172 set_arities = set_arities1, pred_arities = pred_arities1}, |
173 {to_set_simps = to_set_simps2, to_pred_simps = to_pred_simps2, |
173 {to_set_simps = to_set_simps2, to_pred_simps = to_pred_simps2, |
174 set_arities = set_arities2, pred_arities = pred_arities2}) = |
174 set_arities = set_arities2, pred_arities = pred_arities2}) = |
175 {to_set_simps = Drule.merge_rules (to_set_simps1, to_set_simps2), |
175 {to_set_simps = Thm.merge_thms (to_set_simps1, to_set_simps2), |
176 to_pred_simps = Drule.merge_rules (to_pred_simps1, to_pred_simps2), |
176 to_pred_simps = Thm.merge_thms (to_pred_simps1, to_pred_simps2), |
177 set_arities = Symtab.merge_list op = (set_arities1, set_arities2), |
177 set_arities = Symtab.merge_list op = (set_arities1, set_arities2), |
178 pred_arities = Symtab.merge_list op = (pred_arities1, pred_arities2)}; |
178 pred_arities = Symtab.merge_list op = (pred_arities1, pred_arities2)}; |
179 ); |
179 ); |
180 |
180 |
181 fun name_type_of (Free p) = SOME p |
181 fun name_type_of (Free p) = SOME p |