src/Pure/axclass.ML
changeset 36740 6248aa22c694
parent 36610 bafd82950e24
child 36768 46be86127972
--- a/src/Pure/axclass.ML	Sat May 08 14:41:23 2010 +0200
+++ b/src/Pure/axclass.ML	Sat May 08 15:24:59 2010 +0200
@@ -241,7 +241,7 @@
   end;
 
 
-fun the_arity thy a (c, Ss) =
+fun the_arity thy (a, Ss, c) =
   (case AList.lookup (op =) (Symtab.lookup_list (proven_arities_of thy) a) (c, Ss) of
     SOME (thm, _) => Thm.transfer thy thm
   | NONE => error ("Unproven type arity " ^
@@ -295,10 +295,12 @@
   end;
 
 val _ = Context.>> (Context.map_theory
-  (Theory.at_begin complete_classrels #> Theory.at_begin complete_arities));
+  (Theory.at_begin complete_classrels #>
+   Theory.at_begin complete_arities));
 
-val the_classrel_prf = Thm.proof_of oo the_classrel;
-val the_arity_prf = Thm.proof_of ooo the_arity;
+val _ = Proofterm.install_axclass_proofs
+  {classrel_proof = Thm.proof_of oo the_classrel,
+   arity_proof = Thm.proof_of oo the_arity};
 
 
 (* maintain instance parameters *)