# HG changeset patch
# User wenzelm
# Date 1142092569 -3600
# Node ID ff585297e9f50d3cc81fc80ce05d0c91bd5f1e53
# Parent  aa45f5e456d36b5f9894f0631447fd6a465acc97
simplified AxClass interfaces;

diff -r aa45f5e456d3 -r ff585297e9f5 src/HOLCF/pcpodef_package.ML
--- a/src/HOLCF/pcpodef_package.ML	Sat Mar 11 16:53:28 2006 +0100
+++ b/src/HOLCF/pcpodef_package.ML	Sat Mar 11 16:56:09 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 (full_tname, lhs_sorts, ["Porder.sq_ord"])
+      |>> AxClass.prove_arity (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 (full_tname, lhs_sorts, ["Porder.po"])
+           |> AxClass.prove_arity (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 (full_tname, lhs_sorts, ["Pcpo.cpo"])
+          |> AxClass.prove_arity (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 (full_tname, lhs_sorts, ["Pcpo.pcpo"])
+          |> AxClass.prove_arity (full_tname, lhs_sorts, ["Pcpo.pcpo"])
             (Tactic.rtac (typedef_pcpo OF pcpo_thms) 1)
           |> Theory.add_path name
           |> PureThy.add_thms