--- a/src/Pure/axclass.ML Tue Jan 08 10:34:19 2013 +0100
+++ b/src/Pure/axclass.ML Tue Jan 08 12:39:39 2013 +0100
@@ -107,9 +107,8 @@
params2 params1;
(*see Theory.at_begin hook for transitive closure of classrels and arity completion*)
- val proven_classrels' = Symreltab.join (K #1) (proven_classrels1, proven_classrels2);
- val proven_arities' =
- Symtab.join (K (Library.merge (eq_fst op =))) (proven_arities1, proven_arities2);
+ val proven_classrels' = Symreltab.merge (K true) (proven_classrels1, proven_classrels2);
+ val proven_arities' = Symtab.merge_list (eq_fst op =) (proven_arities1, proven_arities2);
val inst_params' =
(Symtab.join (K (Symtab.merge (K true))) (#1 inst_params1, #1 inst_params2),