src/Pure/axclass.ML
changeset 36740 6248aa22c694
parent 36610 bafd82950e24
child 36768 46be86127972
     1.1 --- a/src/Pure/axclass.ML	Sat May 08 14:41:23 2010 +0200
     1.2 +++ b/src/Pure/axclass.ML	Sat May 08 15:24:59 2010 +0200
     1.3 @@ -241,7 +241,7 @@
     1.4    end;
     1.5  
     1.6  
     1.7 -fun the_arity thy a (c, Ss) =
     1.8 +fun the_arity thy (a, Ss, c) =
     1.9    (case AList.lookup (op =) (Symtab.lookup_list (proven_arities_of thy) a) (c, Ss) of
    1.10      SOME (thm, _) => Thm.transfer thy thm
    1.11    | NONE => error ("Unproven type arity " ^
    1.12 @@ -295,10 +295,12 @@
    1.13    end;
    1.14  
    1.15  val _ = Context.>> (Context.map_theory
    1.16 -  (Theory.at_begin complete_classrels #> Theory.at_begin complete_arities));
    1.17 +  (Theory.at_begin complete_classrels #>
    1.18 +   Theory.at_begin complete_arities));
    1.19  
    1.20 -val the_classrel_prf = Thm.proof_of oo the_classrel;
    1.21 -val the_arity_prf = Thm.proof_of ooo the_arity;
    1.22 +val _ = Proofterm.install_axclass_proofs
    1.23 +  {classrel_proof = Thm.proof_of oo the_classrel,
    1.24 +   arity_proof = Thm.proof_of oo the_arity};
    1.25  
    1.26  
    1.27  (* maintain instance parameters *)