# HG changeset patch
# User wenzelm
# Date 1273325099 -7200
# Node ID 6248aa22c694d475514471547fba16d7c577e324
# Parent  e9401d2efc5fa768923e6fd08793c027e2e66c70
back-patching of axclass proofs;

diff -r e9401d2efc5f -r 6248aa22c694 src/Pure/axclass.ML
--- 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 *)
diff -r e9401d2efc5f -r 6248aa22c694 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Sat May 08 14:41:23 2010 +0200
+++ b/src/Pure/proofterm.ML	Sat May 08 15:24:59 2010 +0200
@@ -110,6 +110,11 @@
   val equal_elim: term -> term -> proof -> proof -> proof
   val strip_shyps_proof: Sorts.algebra -> (typ * sort) list -> (typ * sort) list ->
     sort list -> proof -> proof
+  val classrel_proof: theory -> class * class -> proof
+  val arity_proof: theory -> string * sort list * class -> proof
+  val install_axclass_proofs:
+   {classrel_proof: theory -> class * class -> proof,
+    arity_proof: theory -> string * sort list * class -> proof} -> unit
   val axm_proof: string -> term -> proof
   val oracle_proof: string -> term -> oracle * proof
   val promise_proof: theory -> serial -> term -> proof
@@ -886,7 +891,7 @@
   equal_elim_axm %> remove_types A %> remove_types B %% prf1 %% prf2;
 
 
-(**** sort hypotheses ****)
+(**** type classes ****)
 
 fun strip_shyps_proof algebra present witnessed extra_sorts prf =
   let
@@ -902,6 +907,30 @@
   in Same.commit (map_proof_types_same (Term_Subst.map_atypsT_same replace)) prf end;
 
 
+local
+
+type axclass_proofs =
+ {classrel_proof: theory -> class * class -> proof,
+  arity_proof: theory -> string * sort list * class -> proof};
+
+val axclass_proofs: axclass_proofs Single_Assignment.var =
+  Single_Assignment.var "Proofterm.axclass_proofs";
+
+fun axclass_proof which thy x =
+  (case Single_Assignment.peek axclass_proofs of
+    NONE => raise Fail "Axclass proof operations not installed"
+  | SOME prfs => which prfs thy x);
+
+in
+
+val classrel_proof = axclass_proof #classrel_proof;
+val arity_proof = axclass_proof #arity_proof;
+
+fun install_axclass_proofs prfs = Single_Assignment.assign axclass_proofs prfs;
+
+end;
+
+
 (***** axioms and theorems *****)
 
 val proofs = Unsynchronized.ref 2;