# HG changeset patch
# User berghofe
# Date 1140799697 -3600
# Node ID 47d337aefc21c72a1bfc6c81d938c2189b588638
# Parent  7e84a1a3741cdf106842745f76e6f0c849a295c5
Reverted to old interface of AxClass.add_inst_arity(_i)

diff -r 7e84a1a3741c -r 47d337aefc21 src/HOL/Nominal/nominal_atoms.ML
--- a/src/HOL/Nominal/nominal_atoms.ML	Fri Feb 24 09:00:21 2006 +0100
+++ b/src/HOL/Nominal/nominal_atoms.ML	Fri Feb 24 17:48:17 2006 +0100
@@ -401,7 +401,7 @@
 
          in
            thy'
-           |> AxClass.add_inst_arity_i I (qu_name,[],[cls_name])
+           |> AxClass.add_inst_arity_i (qu_name,[],[cls_name])
               (if ak_name = ak_name' then proof1 else proof2)
          end) ak_names thy) ak_names thy12c;
 
@@ -435,15 +435,15 @@
           val pt_thm_set   = pt_inst RS pt_set_inst
        in 
 	thy
-	|> AxClass.add_inst_arity_i I ("fun",[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_fun)
-        |> AxClass.add_inst_arity_i I ("nominal.noption",[[cls_name]],[cls_name]) (pt_proof pt_thm_noptn) 
-        |> AxClass.add_inst_arity_i I ("Datatype.option",[[cls_name]],[cls_name]) (pt_proof pt_thm_optn)
-        |> AxClass.add_inst_arity_i I ("List.list",[[cls_name]],[cls_name]) (pt_proof pt_thm_list)
-        |> AxClass.add_inst_arity_i I ("*",[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_prod)
-        |> AxClass.add_inst_arity_i I ("nominal.nprod",[[cls_name],[cls_name]],[cls_name]) 
+	|> AxClass.add_inst_arity_i ("fun",[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_fun)
+        |> AxClass.add_inst_arity_i ("nominal.noption",[[cls_name]],[cls_name]) (pt_proof pt_thm_noptn) 
+        |> AxClass.add_inst_arity_i ("Datatype.option",[[cls_name]],[cls_name]) (pt_proof pt_thm_optn)
+        |> AxClass.add_inst_arity_i ("List.list",[[cls_name]],[cls_name]) (pt_proof pt_thm_list)
+        |> AxClass.add_inst_arity_i ("*",[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_prod)
+        |> AxClass.add_inst_arity_i ("nominal.nprod",[[cls_name],[cls_name]],[cls_name]) 
                                     (pt_proof pt_thm_nprod)
-        |> AxClass.add_inst_arity_i I ("Product_Type.unit",[],[cls_name]) (pt_proof pt_thm_unit)
-        |> AxClass.add_inst_arity_i I ("set",[[cls_name]],[cls_name]) (pt_proof pt_thm_set)
+        |> AxClass.add_inst_arity_i ("Product_Type.unit",[],[cls_name]) (pt_proof pt_thm_unit)
+        |> AxClass.add_inst_arity_i ("set",[[cls_name]],[cls_name]) (pt_proof pt_thm_set)
      end) ak_names thy13; 
 
        (*<<<<<<<  fs_<ak> class instances  >>>>>>>*)
@@ -476,7 +476,7 @@
                       val simp_s = HOL_basic_ss addsimps [dj_inst RS dj_supp, Finites.emptyI]; 
                   in EVERY [ClassPackage.intro_classes_tac [], asm_simp_tac simp_s 1] end)      
         in 
-	 AxClass.add_inst_arity_i I (qu_name,[],[qu_class]) proof thy' 
+	 AxClass.add_inst_arity_i (qu_name,[],[qu_class]) proof thy' 
         end) ak_names thy) ak_names thy18;
 
        (* shows that                  *)
@@ -500,12 +500,12 @@
           val fs_thm_optn  = fs_inst RS fs_option_inst;
         in 
          thy 
-         |> AxClass.add_inst_arity_i I ("Product_Type.unit",[],[cls_name]) (fs_proof fs_thm_unit) 
-         |> AxClass.add_inst_arity_i I ("*",[[cls_name],[cls_name]],[cls_name]) (fs_proof fs_thm_prod) 
-         |> AxClass.add_inst_arity_i I ("nominal.nprod",[[cls_name],[cls_name]],[cls_name]) 
+         |> AxClass.add_inst_arity_i ("Product_Type.unit",[],[cls_name]) (fs_proof fs_thm_unit) 
+         |> AxClass.add_inst_arity_i ("*",[[cls_name],[cls_name]],[cls_name]) (fs_proof fs_thm_prod) 
+         |> AxClass.add_inst_arity_i ("nominal.nprod",[[cls_name],[cls_name]],[cls_name]) 
                                      (fs_proof fs_thm_nprod) 
-         |> AxClass.add_inst_arity_i I ("List.list",[[cls_name]],[cls_name]) (fs_proof fs_thm_list)
-         |> AxClass.add_inst_arity_i I ("Datatype.option",[[cls_name]],[cls_name]) (fs_proof fs_thm_optn)
+         |> AxClass.add_inst_arity_i ("List.list",[[cls_name]],[cls_name]) (fs_proof fs_thm_list)
+         |> AxClass.add_inst_arity_i ("Datatype.option",[[cls_name]],[cls_name]) (fs_proof fs_thm_optn)
         end) ak_names thy20; 
 
        (*<<<<<<<  cp_<ak>_<ai> class instances  >>>>>>>*)
@@ -551,7 +551,7 @@
                     EVERY [ClassPackage.intro_classes_tac [], simp_tac simp_s 1]
                   end))
 	      in
-                AxClass.add_inst_arity_i I (name,[],[cls_name]) proof thy''
+                AxClass.add_inst_arity_i (name,[],[cls_name]) proof thy''
 	      end) ak_names thy') ak_names thy) ak_names thy24;
       
        (* shows that                                                    *) 
@@ -580,12 +580,12 @@
             val cp_thm_noptn = cp_inst RS cp_noption_inst;
         in
          thy'
-         |> AxClass.add_inst_arity_i I ("Product_Type.unit",[],[cls_name]) (cp_proof cp_thm_unit)
-	 |> AxClass.add_inst_arity_i I ("*",[[cls_name],[cls_name]],[cls_name]) (cp_proof cp_thm_prod)
-         |> AxClass.add_inst_arity_i I ("List.list",[[cls_name]],[cls_name]) (cp_proof cp_thm_list)
-         |> AxClass.add_inst_arity_i I ("fun",[[cls_name],[cls_name]],[cls_name]) (cp_proof cp_thm_fun)
-         |> AxClass.add_inst_arity_i I ("Datatype.option",[[cls_name]],[cls_name]) (cp_proof cp_thm_optn)
-         |> AxClass.add_inst_arity_i I ("nominal.noption",[[cls_name]],[cls_name]) (cp_proof cp_thm_noptn)
+         |> AxClass.add_inst_arity_i ("Product_Type.unit",[],[cls_name]) (cp_proof cp_thm_unit)
+	 |> AxClass.add_inst_arity_i ("*",[[cls_name],[cls_name]],[cls_name]) (cp_proof cp_thm_prod)
+         |> AxClass.add_inst_arity_i ("List.list",[[cls_name]],[cls_name]) (cp_proof cp_thm_list)
+         |> AxClass.add_inst_arity_i ("fun",[[cls_name],[cls_name]],[cls_name]) (cp_proof cp_thm_fun)
+         |> AxClass.add_inst_arity_i ("Datatype.option",[[cls_name]],[cls_name]) (cp_proof cp_thm_optn)
+         |> AxClass.add_inst_arity_i ("nominal.noption",[[cls_name]],[cls_name]) (cp_proof cp_thm_noptn)
         end) ak_names thy) ak_names thy25;
        
      (* show that discrete nominal types are permutation types, finitely     *) 
@@ -601,7 +601,7 @@
 	       val simp_s = HOL_basic_ss addsimps [defn];
                val proof = EVERY [ClassPackage.intro_classes_tac [], REPEAT (asm_simp_tac simp_s 1)];      
              in  
-	       AxClass.add_inst_arity_i I (discrete_ty,[],[qu_class]) proof thy
+	       AxClass.add_inst_arity_i (discrete_ty,[],[qu_class]) proof thy
              end) ak_names;
 
           fun discrete_fs_inst discrete_ty defn = 
@@ -612,7 +612,7 @@
                val simp_s = HOL_ss addsimps [supp_def,Collect_const,Finites.emptyI,defn];
                val proof = EVERY [ClassPackage.intro_classes_tac [], asm_simp_tac simp_s 1];      
              in  
-	       AxClass.add_inst_arity_i I (discrete_ty,[],[qu_class]) proof thy
+	       AxClass.add_inst_arity_i (discrete_ty,[],[qu_class]) proof thy
              end) ak_names;  
 
           fun discrete_cp_inst discrete_ty defn = 
@@ -623,7 +623,7 @@
                val simp_s = HOL_ss addsimps [defn];
                val proof = EVERY [ClassPackage.intro_classes_tac [], asm_simp_tac simp_s 1];      
              in  
-	       AxClass.add_inst_arity_i I (discrete_ty,[],[qu_class]) proof thy
+	       AxClass.add_inst_arity_i (discrete_ty,[],[qu_class]) proof thy
              end) ak_names)) ak_names;  
           
         in
diff -r 7e84a1a3741c -r 47d337aefc21 src/HOL/Nominal/nominal_package.ML
--- a/src/HOL/Nominal/nominal_package.ML	Fri Feb 24 09:00:21 2006 +0100
+++ b/src/HOL/Nominal/nominal_package.ML	Fri Feb 24 17:48:17 2006 +0100
@@ -411,7 +411,7 @@
           (fn _ => EVERY [indtac induction perm_indnames 1,
              ALLGOALS (asm_full_simp_tac simps)])))
       in
-        foldl (fn ((s, tvs), thy) => AxClass.add_inst_arity_i I
+        foldl (fn ((s, tvs), thy) => AxClass.add_inst_arity_i
             (s, replicate (length tvs) (cp_class :: classes), [cp_class])
             (ClassPackage.intro_classes_tac [] THEN ALLGOALS (resolve_tac thms)) thy)
           thy (full_new_type_names' ~~ tyvars)
@@ -420,7 +420,7 @@
     val (perm_thmss,thy3) = thy2 |>
       fold (fn name1 => fold (composition_instance name1) atoms) atoms |>
       curry (Library.foldr (fn ((i, (tyname, args, _)), thy) =>
-        AxClass.add_inst_arity_i I (tyname, replicate (length args) classes, classes)
+        AxClass.add_inst_arity_i (tyname, replicate (length args) classes, classes)
         (ClassPackage.intro_classes_tac [] THEN REPEAT (EVERY
            [resolve_tac perm_empty_thms 1,
             resolve_tac perm_append_thms 1,
@@ -585,7 +585,7 @@
     fun pt_instance ((class, atom), perm_closed_thms) =
       fold (fn (((({Abs_inverse, Rep_inverse, Rep, ...},
         perm_def), name), tvs), perm_closed) => fn thy =>
-          AxClass.add_inst_arity_i I
+          AxClass.add_inst_arity_i
             (Sign.intern_type thy name,
               replicate (length tvs) (classes @ cp_classes), [class])
             (EVERY [ClassPackage.intro_classes_tac [],
@@ -609,7 +609,7 @@
         val cp1' = PureThy.get_thm thy (Name (name ^ "_inst")) RS cp1
       in fold (fn ((((({Abs_inverse, Rep_inverse, Rep, ...},
         perm_def), name), tvs), perm_closed1), perm_closed2) => fn thy =>
-          AxClass.add_inst_arity_i I
+          AxClass.add_inst_arity_i
             (Sign.intern_type thy name,
               replicate (length tvs) (classes @ cp_classes), [class])
             (EVERY [ClassPackage.intro_classes_tac [],
@@ -1086,7 +1086,7 @@
       DatatypeAux.store_thmss_atts "fresh" new_type_names simp_atts fresh_thms ||>
       fold (fn (atom, ths) => fn thy =>
         let val class = Sign.intern_class thy ("fs_" ^ Sign.base_name atom)
-        in fold (fn T => AxClass.add_inst_arity_i I
+        in fold (fn T => AxClass.add_inst_arity_i
             (fst (dest_Type T),
               replicate (length sorts) [class], [class])
             (ClassPackage.intro_classes_tac [] THEN resolve_tac ths 1)) newTs thy
diff -r 7e84a1a3741c -r 47d337aefc21 src/HOLCF/pcpodef_package.ML
--- a/src/HOLCF/pcpodef_package.ML	Fri Feb 24 09:00:21 2006 +0100
+++ b/src/HOLCF/pcpodef_package.ML	Fri Feb 24 17:48:17 2006 +0100
@@ -98,12 +98,12 @@
     fun make_po tac thy =
       thy
       |> TypedefPackage.add_typedef_i def (SOME name) (t, vs, mx) set opt_morphs tac
-      |>> AxClass.add_inst_arity_i I (full_tname, lhs_sorts, ["Porder.sq_ord"])
+      |>> AxClass.add_inst_arity_i (full_tname, lhs_sorts, ["Porder.sq_ord"])
            (ClassPackage.intro_classes_tac [])
       |>>> (PureThy.add_defs_i true [Thm.no_attributes less_def] #> Library.swap)
       |> (fn (thy', ({type_definition, set_def, ...}, [less_definition])) =>
            thy'
-           |> AxClass.add_inst_arity_i I (full_tname, lhs_sorts, ["Porder.po"])
+           |> AxClass.add_inst_arity_i (full_tname, lhs_sorts, ["Porder.po"])
              (Tactic.rtac (typedef_po OF [type_definition, less_definition]) 1)
            |> rpair (type_definition, less_definition, set_def));
     
@@ -113,7 +113,7 @@
         val cpo_thms = [type_def, less_def, admissible'];
         val (_, theory') =
           theory
-          |> AxClass.add_inst_arity_i I (full_tname, lhs_sorts, ["Pcpo.cpo"])
+          |> AxClass.add_inst_arity_i (full_tname, lhs_sorts, ["Pcpo.cpo"])
             (Tactic.rtac (typedef_cpo OF cpo_thms) 1)
           |> Theory.add_path name
           |> PureThy.add_thms
@@ -132,7 +132,7 @@
         val pcpo_thms = [type_def, less_def, UUmem'];
         val (_, theory') =
           theory
-          |> AxClass.add_inst_arity_i I (full_tname, lhs_sorts, ["Pcpo.pcpo"])
+          |> AxClass.add_inst_arity_i (full_tname, lhs_sorts, ["Pcpo.pcpo"])
             (Tactic.rtac (typedef_pcpo OF pcpo_thms) 1)
           |> Theory.add_path name
           |> PureThy.add_thms
diff -r 7e84a1a3741c -r 47d337aefc21 src/Pure/Tools/class_package.ML
--- a/src/Pure/Tools/class_package.ML	Fri Feb 24 09:00:21 2006 +0100
+++ b/src/Pure/Tools/class_package.ML	Fri Feb 24 17:48:17 2006 +0100
@@ -539,7 +539,7 @@
 fun instance_arity_i do_proof = gen_instance_arity AxClass.cert_arity add_defs_overloaded_i
   (K I) do_proof;
 val setup_proof = AxClass.instance_arity_i;
-fun tactic_proof tac after_qed arity = AxClass.add_inst_arity_i after_qed arity tac;
+fun tactic_proof tac after_qed arity = AxClass.add_inst_arity_i arity tac #> after_qed;
 
 in
 
@@ -566,7 +566,7 @@
 fun instance_sort do_proof = gen_add_instance_sort intern_class read_sort do_proof;
 fun instance_sort_i do_proof = gen_add_instance_sort certify_class certify_sort do_proof;
 val setup_proof = AxClass.instance_arity_i I ("", [], []);
-fun tactic_proof tac = AxClass.add_inst_arity_i I ("", [], []) tac;
+fun tactic_proof tac = AxClass.add_inst_arity_i ("", [], []) tac;
 
 in
 
diff -r 7e84a1a3741c -r 47d337aefc21 src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Fri Feb 24 09:00:21 2006 +0100
+++ b/src/Pure/axclass.ML	Fri Feb 24 17:48:17 2006 +0100
@@ -18,10 +18,8 @@
   val add_arity_thms: thm list -> theory -> theory
   val add_inst_subclass: xstring * xstring -> tactic -> theory -> theory
   val add_inst_subclass_i: class * class -> tactic -> theory -> theory
-  val add_inst_arity: (theory -> theory) ->
-    xstring * string list * string -> tactic -> theory -> theory
-  val add_inst_arity_i: (theory -> theory) ->
-    string * sort list * sort -> tactic -> theory -> theory
+  val add_inst_arity: xstring * string list * string -> tactic -> theory -> theory
+  val add_inst_arity_i: string * sort list * sort -> tactic -> theory -> theory
   val instance_subclass: xstring * xstring -> theory -> Proof.state
   val instance_subclass_i: class * class -> theory -> Proof.state
   val instance_arity: (theory -> theory) -> xstring * string list * string -> theory -> Proof.state
@@ -278,7 +276,7 @@
       cat_error msg ("The error(s) above occurred while trying to prove " ^ txt);
   in add_classrel_thms [th] thy end;
 
-fun ext_inst_arity prep_arity (after_qed : theory -> theory) raw_arity tac thy =
+fun ext_inst_arity prep_arity raw_arity tac thy =
   let
     val arity = prep_arity thy raw_arity;
     val txt = quote (Sign.string_of_arity thy arity);
@@ -287,11 +285,7 @@
     val ths = Goal.prove_multi thy [] [] props
       (fn _ => Tactic.precise_conjunction_tac (length props) 1 THEN tac) handle ERROR msg =>
         cat_error msg ("\nThe error(s) above occurred while trying to prove " ^ txt);
-  in
-    thy
-    |> add_arity_thms ths
-    |> after_qed
-  end;
+  in add_arity_thms ths thy end;
 
 in