src/HOLCF/pcpodef_package.ML

       | option_fold_rule (SOME def) = fold_rule [def];
     
     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));
     
     fun make_cpo admissible (theory, defs as (type_def, less_def, set_def)) =
       let
         val admissible' = option_fold_rule set_def admissible;
         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
             ([(("adm_" ^ name, admissible'), []),
               (("cont_" ^ Rep_name, cont_Rep OF cpo_thms), []),

       let
         val UUmem' = option_fold_rule set_def UUmem;
         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
             ([((Rep_name ^ "_strict", Rep_strict OF pcpo_thms), []),
               ((Abs_name ^ "_strict", Abs_strict OF pcpo_thms), []),