more standard module name Axclass (according to file name);
authorwenzelm
Wed Apr 10 15:30:19 2013 +0200 (2013-04-10)
changeset 51685385ef6706252
parent 51671 0d142a78fb7c
child 51686 532e0ac5a66d
more standard module name Axclass (according to file name);
src/Doc/more_antiquote.ML
src/HOL/HOLCF/Tools/Domain/domain.ML
src/HOL/HOLCF/Tools/Domain/domain_axioms.ML
src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML
src/HOL/HOLCF/Tools/cpodef.ML
src/HOL/Library/refute.ML
src/HOL/Nominal/nominal_atoms.ML
src/HOL/Nominal/nominal_datatype.ML
src/HOL/Tools/Datatype/datatype_codegen.ML
src/HOL/Tools/Nitpick/nitpick_preproc.ML
src/HOL/Tools/Predicate_Compile/predicate_compile.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML
src/HOL/Tools/Quickcheck/narrowing_generators.ML
src/HOL/Tools/code_evaluation.ML
src/HOL/Tools/record.ML
src/Pure/Isar/class.ML
src/Pure/Isar/class_declaration.ML
src/Pure/Isar/code.ML
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/typedecl.ML
src/Pure/axclass.ML
src/Tools/Code/code_preproc.ML
src/Tools/Code/code_target.ML
src/Tools/Code/code_thingol.ML
src/Tools/nbe.ML
     1.1 --- a/src/Doc/more_antiquote.ML	Wed Apr 10 13:10:38 2013 +0200
     1.2 +++ b/src/Doc/more_antiquote.ML	Wed Apr 10 15:30:19 2013 +0200
     1.3 @@ -36,7 +36,7 @@
     1.4        |> Code.equations_of_cert thy
     1.5        |> snd
     1.6        |> map_filter (fn (_, (some_thm, proper)) => if proper then some_thm else NONE)
     1.7 -      |> map (holize o no_vars ctxt o AxClass.overload thy);
     1.8 +      |> map (holize o no_vars ctxt o Axclass.overload thy);
     1.9    in Thy_Output.output ctxt (Thy_Output.maybe_pretty_source pretty_thm ctxt src thms) end;
    1.10  
    1.11  in
     2.1 --- a/src/HOL/HOLCF/Tools/Domain/domain.ML	Wed Apr 10 13:10:38 2013 +0200
     2.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain.ML	Wed Apr 10 15:30:19 2013 +0200
     2.3 @@ -44,7 +44,7 @@
     2.4  fun add_arity ((b, sorts, mx), sort) thy : theory =
     2.5    thy
     2.6    |> Sign.add_types_global [(b, length sorts, mx)]
     2.7 -  |> AxClass.axiomatize_arity (Sign.full_name thy b, sorts, sort)
     2.8 +  |> Axclass.axiomatize_arity (Sign.full_name thy b, sorts, sort)
     2.9  
    2.10  fun gen_add_domain
    2.11      (prep_sort : theory -> 'a -> sort)
     3.1 --- a/src/HOL/HOLCF/Tools/Domain/domain_axioms.ML	Wed Apr 10 13:10:38 2013 +0200
     3.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain_axioms.ML	Wed Apr 10 15:30:19 2013 +0200
     3.3 @@ -104,7 +104,7 @@
     3.4      fun thy_arity (_, _, (lhsT, _)) =
     3.5          let val (dname, tvars) = dest_Type lhsT
     3.6          in (dname, map (snd o dest_TFree) tvars, @{sort pcpo}) end
     3.7 -    val thy = fold (AxClass.axiomatize_arity o thy_arity) dom_eqns thy
     3.8 +    val thy = fold (Axclass.axiomatize_arity o thy_arity) dom_eqns thy
     3.9  
    3.10      (* declare and axiomatize abs/rep *)
    3.11      val (iso_infos, thy) =
     4.1 --- a/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Wed Apr 10 13:10:38 2013 +0200
     4.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Wed Apr 10 15:30:19 2013 +0200
     4.3 @@ -427,7 +427,7 @@
     4.4          fun arity (vs, tbind, _, _, _) =
     4.5            (Sign.full_name thy tbind, map the_sort vs, @{sort "domain"})
     4.6        in
     4.7 -        fold AxClass.axiomatize_arity (map arity doms) tmp_thy
     4.8 +        fold Axclass.axiomatize_arity (map arity doms) tmp_thy
     4.9        end
    4.10  
    4.11      (* check bifiniteness of right-hand sides *)
     5.1 --- a/src/HOL/HOLCF/Tools/cpodef.ML	Wed Apr 10 13:10:38 2013 +0200
     5.2 +++ b/src/HOL/HOLCF/Tools/cpodef.ML	Wed Apr 10 15:30:19 2013 +0200
     5.3 @@ -74,7 +74,7 @@
     5.4      val (full_tname, Ts) = dest_Type newT
     5.5      val lhs_sorts = map (snd o dest_TFree) Ts
     5.6      val tac = Tactic.rtac (@{thm typedef_cpo} OF cpo_thms) 1
     5.7 -    val thy = AxClass.prove_arity (full_tname, lhs_sorts, @{sort cpo}) (K tac) thy
     5.8 +    val thy = Axclass.prove_arity (full_tname, lhs_sorts, @{sort cpo}) (K tac) thy
     5.9      (* transfer thms so that they will know about the new cpo instance *)
    5.10      val cpo_thms' = map (Thm.transfer thy) cpo_thms
    5.11      fun make thm = Drule.zero_var_indexes (thm OF cpo_thms')
    5.12 @@ -113,7 +113,7 @@
    5.13      val (full_tname, Ts) = dest_Type newT
    5.14      val lhs_sorts = map (snd o dest_TFree) Ts
    5.15      val tac = Tactic.rtac (@{thm typedef_pcpo} OF pcpo_thms) 1
    5.16 -    val thy = AxClass.prove_arity (full_tname, lhs_sorts, @{sort pcpo}) (K tac) thy
    5.17 +    val thy = Axclass.prove_arity (full_tname, lhs_sorts, @{sort pcpo}) (K tac) thy
    5.18      val pcpo_thms' = map (Thm.transfer thy) pcpo_thms
    5.19      fun make thm = Drule.zero_var_indexes (thm OF pcpo_thms')
    5.20      val Rep_strict = make @{thm typedef_Rep_strict}
     6.1 --- a/src/HOL/Library/refute.ML	Wed Apr 10 13:10:38 2013 +0200
     6.2 +++ b/src/HOL/Library/refute.ML	Wed Apr 10 15:30:19 2013 +0200
     6.3 @@ -695,7 +695,7 @@
     6.4          val superclasses = distinct (op =) superclasses
     6.5          val class_axioms = maps (fn class => map (fn ax =>
     6.6            ("<" ^ class ^ ">", Thm.prop_of ax))
     6.7 -          (#axioms (AxClass.get_info thy class) handle ERROR _ => []))
     6.8 +          (#axioms (Axclass.get_info thy class) handle ERROR _ => []))
     6.9            superclasses
    6.10          (* replace the (at most one) schematic type variable in each axiom *)
    6.11          (* by the actual type 'T'                                          *)
     7.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Wed Apr 10 13:10:38 2013 +0200
     7.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Wed Apr 10 15:30:19 2013 +0200
     7.3 @@ -311,7 +311,7 @@
     7.4                         (HOLogic.mk_Trueprop (cprm_eq $ pi1 $ pi2),
     7.5                          HOLogic.mk_Trueprop (HOLogic.mk_eq (cperm $ pi1 $ x, cperm $ pi2 $ x)));
     7.6        in
     7.7 -          AxClass.define_class (Binding.name cl_name, ["HOL.type"]) []
     7.8 +          Axclass.define_class (Binding.name cl_name, ["HOL.type"]) []
     7.9                  [((Binding.name (cl_name ^ "1"), [Simplifier.simp_add]), [axiom1]),
    7.10                   ((Binding.name (cl_name ^ "2"), []), [axiom2]),                           
    7.11                   ((Binding.name (cl_name ^ "3"), []), [axiom3])] thy
    7.12 @@ -360,7 +360,7 @@
    7.13            val axiom1   = HOLogic.mk_Trueprop (cfinite $ (csupp $ x));
    7.14  
    7.15         in  
    7.16 -        AxClass.define_class (Binding.name cl_name, [pt_name]) []
    7.17 +        Axclass.define_class (Binding.name cl_name, [pt_name]) []
    7.18            [((Binding.name (cl_name ^ "1"), []), [axiom1])] thy
    7.19         end) ak_names_types thy8; 
    7.20           
    7.21 @@ -410,7 +410,7 @@
    7.22                             (HOLogic.mk_eq (cperm1 $ pi1 $ (cperm2 $ pi2 $ x), 
    7.23                                             cperm2 $ (cperm3 $ pi1 $ pi2) $ (cperm1 $ pi1 $ x)));
    7.24                 in  
    7.25 -                 AxClass.define_class (Binding.name cl_name, ["HOL.type"]) []
    7.26 +                 Axclass.define_class (Binding.name cl_name, ["HOL.type"]) []
    7.27                     [((Binding.name (cl_name ^ "1"), []), [ax1])] thy'  
    7.28                 end) ak_names_types thy) ak_names_types thy12;
    7.29  
    7.30 @@ -517,7 +517,7 @@
    7.31  
    7.32           in
    7.33             thy'
    7.34 -           |> AxClass.prove_arity (qu_name,[],[cls_name])
    7.35 +           |> Axclass.prove_arity (qu_name,[],[cls_name])
    7.36                (fn _ => if ak_name = ak_name' then proof1 else proof2)
    7.37           end) ak_names thy) ak_names thy12d;
    7.38  
    7.39 @@ -551,15 +551,15 @@
    7.40            val pt_thm_unit  = pt_unit_inst;
    7.41         in
    7.42          thy
    7.43 -        |> AxClass.prove_arity ("fun",[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_fun)
    7.44 -        |> AxClass.prove_arity (@{type_name Set.set},[[cls_name]],[cls_name]) (pt_proof pt_thm_set)
    7.45 -        |> AxClass.prove_arity ("Nominal.noption",[[cls_name]],[cls_name]) (pt_proof pt_thm_noptn) 
    7.46 -        |> AxClass.prove_arity ("Option.option",[[cls_name]],[cls_name]) (pt_proof pt_thm_optn)
    7.47 -        |> AxClass.prove_arity ("List.list",[[cls_name]],[cls_name]) (pt_proof pt_thm_list)
    7.48 -        |> AxClass.prove_arity (@{type_name Product_Type.prod},[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_prod)
    7.49 -        |> AxClass.prove_arity ("Nominal.nprod",[[cls_name],[cls_name]],[cls_name]) 
    7.50 +        |> Axclass.prove_arity ("fun",[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_fun)
    7.51 +        |> Axclass.prove_arity (@{type_name Set.set},[[cls_name]],[cls_name]) (pt_proof pt_thm_set)
    7.52 +        |> Axclass.prove_arity ("Nominal.noption",[[cls_name]],[cls_name]) (pt_proof pt_thm_noptn) 
    7.53 +        |> Axclass.prove_arity ("Option.option",[[cls_name]],[cls_name]) (pt_proof pt_thm_optn)
    7.54 +        |> Axclass.prove_arity ("List.list",[[cls_name]],[cls_name]) (pt_proof pt_thm_list)
    7.55 +        |> Axclass.prove_arity (@{type_name Product_Type.prod},[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_prod)
    7.56 +        |> Axclass.prove_arity ("Nominal.nprod",[[cls_name],[cls_name]],[cls_name]) 
    7.57                                      (pt_proof pt_thm_nprod)
    7.58 -        |> AxClass.prove_arity ("Product_Type.unit",[],[cls_name]) (pt_proof pt_thm_unit)
    7.59 +        |> Axclass.prove_arity ("Product_Type.unit",[],[cls_name]) (pt_proof pt_thm_unit)
    7.60       end) ak_names thy13; 
    7.61  
    7.62         (********  fs_<ak> class instances  ********)
    7.63 @@ -592,7 +592,7 @@
    7.64                        val simp_s = HOL_basic_ss addsimps [dj_inst RS dj_supp, finite_emptyI];
    7.65                    in EVERY [Class.intro_classes_tac [], asm_simp_tac simp_s 1] end)
    7.66          in
    7.67 -         AxClass.prove_arity (qu_name,[],[qu_class]) (fn _ => proof) thy'
    7.68 +         Axclass.prove_arity (qu_name,[],[qu_class]) (fn _ => proof) thy'
    7.69          end) ak_names thy) ak_names thy18;
    7.70  
    7.71         (* shows that                  *)
    7.72 @@ -616,12 +616,12 @@
    7.73            val fs_thm_optn  = fs_inst RS fs_option_inst;
    7.74          in 
    7.75           thy
    7.76 -         |> AxClass.prove_arity ("Product_Type.unit",[],[cls_name]) (fs_proof fs_thm_unit) 
    7.77 -         |> AxClass.prove_arity (@{type_name Product_Type.prod},[[cls_name],[cls_name]],[cls_name]) (fs_proof fs_thm_prod) 
    7.78 -         |> AxClass.prove_arity ("Nominal.nprod",[[cls_name],[cls_name]],[cls_name]) 
    7.79 +         |> Axclass.prove_arity ("Product_Type.unit",[],[cls_name]) (fs_proof fs_thm_unit) 
    7.80 +         |> Axclass.prove_arity (@{type_name Product_Type.prod},[[cls_name],[cls_name]],[cls_name]) (fs_proof fs_thm_prod) 
    7.81 +         |> Axclass.prove_arity ("Nominal.nprod",[[cls_name],[cls_name]],[cls_name]) 
    7.82                                       (fs_proof fs_thm_nprod) 
    7.83 -         |> AxClass.prove_arity ("List.list",[[cls_name]],[cls_name]) (fs_proof fs_thm_list)
    7.84 -         |> AxClass.prove_arity ("Option.option",[[cls_name]],[cls_name]) (fs_proof fs_thm_optn)
    7.85 +         |> Axclass.prove_arity ("List.list",[[cls_name]],[cls_name]) (fs_proof fs_thm_list)
    7.86 +         |> Axclass.prove_arity ("Option.option",[[cls_name]],[cls_name]) (fs_proof fs_thm_optn)
    7.87          end) ak_names thy20;
    7.88  
    7.89         (********  cp_<ak>_<ai> class instances  ********)
    7.90 @@ -669,7 +669,7 @@
    7.91                      EVERY [Class.intro_classes_tac [], simp_tac simp_s 1]
    7.92                    end))
    7.93                in
    7.94 -                AxClass.prove_arity (name,[],[cls_name]) (fn _ => proof) thy''
    7.95 +                Axclass.prove_arity (name,[],[cls_name]) (fn _ => proof) thy''
    7.96                end) ak_names thy') ak_names thy) ak_names thy24;
    7.97  
    7.98         (* shows that                                                    *) 
    7.99 @@ -700,13 +700,13 @@
   7.100              val cp_thm_set = cp_inst RS cp_set_inst;
   7.101          in
   7.102           thy'
   7.103 -         |> AxClass.prove_arity ("Product_Type.unit",[],[cls_name]) (cp_proof cp_thm_unit)
   7.104 -         |> AxClass.prove_arity (@{type_name Product_Type.prod}, [[cls_name],[cls_name]],[cls_name]) (cp_proof cp_thm_prod)
   7.105 -         |> AxClass.prove_arity ("List.list",[[cls_name]],[cls_name]) (cp_proof cp_thm_list)
   7.106 -         |> AxClass.prove_arity ("fun",[[cls_name],[cls_name]],[cls_name]) (cp_proof cp_thm_fun)
   7.107 -         |> AxClass.prove_arity ("Option.option",[[cls_name]],[cls_name]) (cp_proof cp_thm_optn)
   7.108 -         |> AxClass.prove_arity ("Nominal.noption",[[cls_name]],[cls_name]) (cp_proof cp_thm_noptn)
   7.109 -         |> AxClass.prove_arity (@{type_name Set.set},[[cls_name]],[cls_name]) (cp_proof cp_thm_set)
   7.110 +         |> Axclass.prove_arity ("Product_Type.unit",[],[cls_name]) (cp_proof cp_thm_unit)
   7.111 +         |> Axclass.prove_arity (@{type_name Product_Type.prod}, [[cls_name],[cls_name]],[cls_name]) (cp_proof cp_thm_prod)
   7.112 +         |> Axclass.prove_arity ("List.list",[[cls_name]],[cls_name]) (cp_proof cp_thm_list)
   7.113 +         |> Axclass.prove_arity ("fun",[[cls_name],[cls_name]],[cls_name]) (cp_proof cp_thm_fun)
   7.114 +         |> Axclass.prove_arity ("Option.option",[[cls_name]],[cls_name]) (cp_proof cp_thm_optn)
   7.115 +         |> Axclass.prove_arity ("Nominal.noption",[[cls_name]],[cls_name]) (cp_proof cp_thm_noptn)
   7.116 +         |> Axclass.prove_arity (@{type_name Set.set},[[cls_name]],[cls_name]) (cp_proof cp_thm_set)
   7.117          end) ak_names thy) ak_names thy25;
   7.118  
   7.119       (* show that discrete nominal types are permutation types, finitely     *)
   7.120 @@ -722,7 +722,7 @@
   7.121                 val simp_s = HOL_basic_ss addsimps [Simpdata.mk_eq defn];
   7.122                 val proof = EVERY [Class.intro_classes_tac [], REPEAT (asm_simp_tac simp_s 1)];
   7.123               in 
   7.124 -               AxClass.prove_arity (discrete_ty, [], [qu_class]) (fn _ => proof) thy
   7.125 +               Axclass.prove_arity (discrete_ty, [], [qu_class]) (fn _ => proof) thy
   7.126               end) ak_names;
   7.127  
   7.128            fun discrete_fs_inst discrete_ty defn = 
   7.129 @@ -733,7 +733,7 @@
   7.130                 val simp_s = HOL_ss addsimps [supp_def, Collect_const, finite_emptyI, Simpdata.mk_eq defn];
   7.131                 val proof = EVERY [Class.intro_classes_tac [], asm_simp_tac simp_s 1];
   7.132               in 
   7.133 -               AxClass.prove_arity (discrete_ty, [], [qu_class]) (fn _ => proof) thy
   7.134 +               Axclass.prove_arity (discrete_ty, [], [qu_class]) (fn _ => proof) thy
   7.135               end) ak_names;
   7.136  
   7.137            fun discrete_cp_inst discrete_ty defn = 
   7.138 @@ -744,7 +744,7 @@
   7.139                 val simp_s = HOL_ss addsimps [Simpdata.mk_eq defn];
   7.140                 val proof = EVERY [Class.intro_classes_tac [], asm_simp_tac simp_s 1];
   7.141               in
   7.142 -               AxClass.prove_arity (discrete_ty, [], [qu_class]) (fn _ => proof) thy
   7.143 +               Axclass.prove_arity (discrete_ty, [], [qu_class]) (fn _ => proof) thy
   7.144               end) ak_names)) ak_names;
   7.145  
   7.146          in
     8.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Wed Apr 10 13:10:38 2013 +0200
     8.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Wed Apr 10 15:30:19 2013 +0200
     8.3 @@ -425,7 +425,7 @@
     8.4            (fn {context = ctxt, ...} => EVERY [Datatype_Aux.ind_tac induct perm_indnames 1,
     8.5               ALLGOALS (asm_full_simp_tac (simps ctxt))]))
     8.6        in
     8.7 -        fold (fn (s, tvs) => fn thy => AxClass.prove_arity
     8.8 +        fold (fn (s, tvs) => fn thy => Axclass.prove_arity
     8.9              (s, map (inter_sort thy sort o snd) tvs, [cp_class])
    8.10              (fn _ => Class.intro_classes_tac [] THEN ALLGOALS (resolve_tac thms)) thy)
    8.11            (full_new_type_names' ~~ tyvars) thy
    8.12 @@ -437,7 +437,7 @@
    8.13        fold (fn atom => fn thy =>
    8.14          let val pt_name = pt_class_of thy atom
    8.15          in
    8.16 -          fold (fn (s, tvs) => fn thy => AxClass.prove_arity
    8.17 +          fold (fn (s, tvs) => fn thy => Axclass.prove_arity
    8.18                (s, map (inter_sort thy [pt_name] o snd) tvs, [pt_name])
    8.19                (fn _ => EVERY
    8.20                  [Class.intro_classes_tac [],
    8.21 @@ -618,7 +618,7 @@
    8.22              val pt_class = pt_class_of thy atom;
    8.23              val sort = Sign.minimize_sort thy (Sign.certify_sort thy
    8.24                (pt_class :: map (cp_class_of thy atom) (remove (op =) atom dt_atoms)))
    8.25 -          in AxClass.prove_arity
    8.26 +          in Axclass.prove_arity
    8.27              (Sign.intern_type thy name,
    8.28                map (inter_sort thy sort o snd) tvs, [pt_class])
    8.29              (fn ctxt => EVERY [Class.intro_classes_tac [],
    8.30 @@ -648,7 +648,7 @@
    8.31          val cp1' = cp_inst_of thy atom1 atom2 RS cp1
    8.32        in fold (fn ((((((Abs_inverse, Rep),
    8.33          perm_def), name), tvs), perm_closed1), perm_closed2) => fn thy =>
    8.34 -          AxClass.prove_arity
    8.35 +          Axclass.prove_arity
    8.36              (Sign.intern_type thy name,
    8.37                map (inter_sort thy sort o snd) tvs, [cp_class])
    8.38              (fn ctxt => EVERY [Class.intro_classes_tac [],
    8.39 @@ -1105,7 +1105,7 @@
    8.40          let
    8.41            val class = fs_class_of thy atom;
    8.42            val sort = Sign.minimize_sort thy (Sign.certify_sort thy (class :: pt_cp_sort));
    8.43 -        in fold (fn Type (s, Ts) => AxClass.prove_arity
    8.44 +        in fold (fn Type (s, Ts) => Axclass.prove_arity
    8.45            (s, map (inter_sort thy sort o snd o dest_TFree) Ts, [class])
    8.46            (fn _ => Class.intro_classes_tac [] THEN resolve_tac ths 1)) newTs thy
    8.47          end) (atoms ~~ finite_supp_thms) ||>
     9.1 --- a/src/HOL/Tools/Datatype/datatype_codegen.ML	Wed Apr 10 13:10:38 2013 +0200
     9.2 +++ b/src/HOL/Tools/Datatype/datatype_codegen.ML	Wed Apr 10 15:30:19 2013 +0200
     9.3 @@ -19,7 +19,7 @@
     9.4  fun mk_constr_consts thy vs tyco cos =
     9.5    let
     9.6      val cs = map (fn (c, tys) => (c, tys ---> Type (tyco, map TFree vs))) cos;
     9.7 -    val cs' = map (fn c_ty as (_, ty) => (AxClass.unoverload_const thy c_ty, ty)) cs;
     9.8 +    val cs' = map (fn c_ty as (_, ty) => (Axclass.unoverload_const thy c_ty, ty)) cs;
     9.9    in
    9.10      if is_some (try (Code.constrset_of_consts thy) cs')
    9.11      then SOME cs
    9.12 @@ -54,7 +54,7 @@
    9.13      |> Raw_Simplifier.rewrite_rule [Thm.symmetric (Thm.assume asm)]
    9.14      |> Thm.implies_intr asm
    9.15      |> Thm.generalize ([], params) 0
    9.16 -    |> AxClass.unoverload thy
    9.17 +    |> Axclass.unoverload thy
    9.18      |> Thm.varifyT_global
    9.19    end;
    9.20  
    10.1 --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Wed Apr 10 13:10:38 2013 +0200
    10.2 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Wed Apr 10 15:30:19 2013 +0200
    10.3 @@ -1028,7 +1028,7 @@
    10.4        let
    10.5          val supers = Sign.complete_sort thy S
    10.6          val class_axioms =
    10.7 -          maps (fn class => map prop_of (AxClass.get_info thy class |> #axioms
    10.8 +          maps (fn class => map prop_of (Axclass.get_info thy class |> #axioms
    10.9                                           handle ERROR _ => [])) supers
   10.10          val monomorphic_class_axioms =
   10.11            map (fn t => case Term.add_tvars t [] of
    11.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Wed Apr 10 13:10:38 2013 +0200
    11.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Wed Apr 10 15:30:19 2013 +0200
    11.3 @@ -36,7 +36,7 @@
    11.4        ^ (space_implode "\n" (map (Display.string_of_thm_global thy) thms)) ^ "\n") specs
    11.5      |> space_implode "\n" |> tracing
    11.6    else ()
    11.7 -fun overload_const thy s = the_default s (Option.map fst (AxClass.inst_of_param thy s))
    11.8 +fun overload_const thy s = the_default s (Option.map fst (Axclass.inst_of_param thy s))
    11.9  
   11.10  fun map_specs f specs =
   11.11    map (fn (s, ths) => (s, f ths)) specs
   11.12 @@ -109,7 +109,7 @@
   11.13        val intross5 = map_specs (map (remove_equalities thy2)) intross4
   11.14        val _ = print_intross options thy2 "After removing equality premises:" intross5
   11.15        val intross6 =
   11.16 -        map (fn (s, ths) => (overload_const thy2 s, map (AxClass.overload thy2) ths)) intross5
   11.17 +        map (fn (s, ths) => (overload_const thy2 s, map (Axclass.overload thy2) ths)) intross5
   11.18        val intross7 = map_specs (map (expand_tuples thy2)) intross6
   11.19        val intross8 = map_specs (map (eta_contract_ho_arguments thy2)) intross7
   11.20        val _ = case !intro_hook of NONE => () | SOME f => (map_specs (map (f thy2)) intross8; ())
    12.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Wed Apr 10 13:10:38 2013 +0200
    12.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Wed Apr 10 15:30:19 2013 +0200
    12.3 @@ -189,7 +189,7 @@
    12.4  fun get_specification options thy t =
    12.5    let
    12.6      (*val (c, T) = dest_Const t
    12.7 -    val t = Const (AxClass.unoverload_const thy (c, T), T)*)
    12.8 +    val t = Const (Axclass.unoverload_const thy (c, T), T)*)
    12.9      val _ = if show_steps options then
   12.10          tracing ("getting specification of " ^ Syntax.string_of_term_global thy t ^
   12.11            " with type " ^ Syntax.string_of_typ_global thy (fastype_of t))
    13.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Wed Apr 10 13:10:38 2013 +0200
    13.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Wed Apr 10 15:30:19 2013 +0200
    13.3 @@ -93,7 +93,7 @@
    13.4      val ty = Type (tyco, map TFree vs);
    13.5      val cs = (map o apsnd o apsnd o map o map_atyps)
    13.6        (fn TFree (v, _) => TFree (v, (the o AList.lookup (op =) vs) v)) raw_cs;
    13.7 -    val const = AxClass.param_of_inst thy (@{const_name partial_term_of}, tyco);
    13.8 +    val const = Axclass.param_of_inst thy (@{const_name partial_term_of}, tyco);
    13.9      val var_insts =
   13.10        map (SOME o Thm.cterm_of thy o Logic.unvarify_types_global o Logic.varify_global)
   13.11          [Free ("ty", Term.itselfT ty), @{term "Quickcheck_Narrowing.Narrowing_variable p tt"},
    14.1 --- a/src/HOL/Tools/code_evaluation.ML	Wed Apr 10 13:10:38 2013 +0200
    14.2 +++ b/src/HOL/Tools/code_evaluation.ML	Wed Apr 10 15:30:19 2013 +0200
    14.3 @@ -78,7 +78,7 @@
    14.4      val ty = Type (tyco, map TFree vs);
    14.5      val cs = (map o apsnd o apsnd o map o map_atyps)
    14.6        (fn TFree (v, _) => TFree (v, (the o AList.lookup (op =) vs) v)) raw_cs;
    14.7 -    val const = AxClass.param_of_inst thy (@{const_name term_of}, tyco);
    14.8 +    val const = Axclass.param_of_inst thy (@{const_name term_of}, tyco);
    14.9      val eqs = map (mk_term_of_eq thy ty) cs;
   14.10   in
   14.11      thy
   14.12 @@ -115,7 +115,7 @@
   14.13      val ty = Type (tyco, map TFree vs);
   14.14      val ty_rep = map_atyps
   14.15        (fn TFree (v, _) => TFree (v, (the o AList.lookup (op =) vs) v)) raw_ty_rep;
   14.16 -    val const = AxClass.param_of_inst thy (@{const_name term_of}, tyco);
   14.17 +    val const = Axclass.param_of_inst thy (@{const_name term_of}, tyco);
   14.18      val eq = mk_abs_term_of_eq thy ty abs ty_rep proj;
   14.19   in
   14.20      thy
   14.21 @@ -169,7 +169,7 @@
   14.22  
   14.23  fun mk_term_of t = HOLogic.mk_term_of (fastype_of t) t;
   14.24  
   14.25 -fun term_of_const_for thy = AxClass.unoverload_const thy o dest_Const o HOLogic.term_of_const;
   14.26 +fun term_of_const_for thy = Axclass.unoverload_const thy o dest_Const o HOLogic.term_of_const;
   14.27  
   14.28  fun gen_dynamic_value dynamic_value thy t =
   14.29    dynamic_value cookie thy NONE I (mk_term_of t) [];
   14.30 @@ -204,7 +204,7 @@
   14.31  fun static_conv thy consts Ts =
   14.32    let
   14.33      val eqs = "==" :: @{const_name HOL.eq} ::
   14.34 -      map (fn T => AxClass.unoverload_const thy (@{const_name HOL.equal}, T)) Ts;
   14.35 +      map (fn T => Axclass.unoverload_const thy (@{const_name HOL.equal}, T)) Ts;
   14.36          (*assumes particular code equations for "==" etc.*)
   14.37    in
   14.38      certify_eval thy (static_value thy consts Ts)
    15.1 --- a/src/HOL/Tools/record.ML	Wed Apr 10 13:10:38 2013 +0200
    15.2 +++ b/src/HOL/Tools/record.ML	Wed Apr 10 15:30:19 2013 +0200
    15.3 @@ -1746,12 +1746,12 @@
    15.4          THEN ALLGOALS (rtac @{thm refl});
    15.5        fun mk_eq thy eq_def =
    15.6          Simplifier.rewrite_rule
    15.7 -          [AxClass.unoverload thy (Thm.symmetric (Simpdata.mk_eq eq_def))] inject;
    15.8 +          [Axclass.unoverload thy (Thm.symmetric (Simpdata.mk_eq eq_def))] inject;
    15.9        fun mk_eq_refl thy =
   15.10          @{thm equal_refl}
   15.11          |> Thm.instantiate
   15.12            ([pairself (ctyp_of thy) (TVar (("'a", 0), @{sort equal}), Logic.varifyT_global extT)], [])
   15.13 -        |> AxClass.unoverload thy;
   15.14 +        |> Axclass.unoverload thy;
   15.15        val ensure_random_record = ensure_sort_record (@{sort random}, mk_random_eq);
   15.16        val ensure_exhaustive_record =
   15.17          ensure_sort_record (@{sort full_exhaustive}, mk_full_exhaustive_eq);
    16.1 --- a/src/Pure/Isar/class.ML	Wed Apr 10 13:10:38 2013 +0200
    16.2 +++ b/src/Pure/Isar/class.ML	Wed Apr 10 15:30:19 2013 +0200
    16.3 @@ -127,7 +127,7 @@
    16.4    let
    16.5      fun params class =
    16.6        let
    16.7 -        val const_typs = (#params o AxClass.get_info thy) class;
    16.8 +        val const_typs = (#params o Axclass.get_info thy) class;
    16.9          val const_names = (#consts o the_class_data thy) class;
   16.10        in
   16.11          (map o apsnd)
   16.12 @@ -190,7 +190,7 @@
   16.13          ([Pretty.command "class", Pretty.brk 1,
   16.14            Pretty.mark_str (Name_Space.markup_extern ctxt class_space class), Pretty.str ":",
   16.15            Pretty.fbrk, Pretty.block [Pretty.str "supersort: ", prt_supersort class]] @
   16.16 -          (case try (AxClass.get_info thy) class of
   16.17 +          (case try (Axclass.get_info thy) class of
   16.18              NONE => []
   16.19            | SOME {params, ...} =>
   16.20                [Pretty.fbrk, Pretty.big_list "parameters:" (map prt_param params)]) @
   16.21 @@ -263,7 +263,7 @@
   16.22        | NONE => I);
   16.23    in
   16.24      thy
   16.25 -    |> AxClass.add_classrel classrel
   16.26 +    |> Axclass.add_classrel classrel
   16.27      |> Class_Data.map (Graph.add_edge (sub, sup))
   16.28      |> activate_defs sub (these_defs thy diff_sort)
   16.29      |> add_dependency
   16.30 @@ -401,7 +401,7 @@
   16.31  fun gen_classrel mk_prop classrel thy =
   16.32    let
   16.33      fun after_qed results =
   16.34 -      Proof_Context.background_theory ((fold o fold) AxClass.add_classrel results);
   16.35 +      Proof_Context.background_theory ((fold o fold) Axclass.add_classrel results);
   16.36    in
   16.37      thy
   16.38      |> Proof_Context.init_global
   16.39 @@ -411,9 +411,9 @@
   16.40  in
   16.41  
   16.42  val classrel =
   16.43 -  gen_classrel (Logic.mk_classrel oo AxClass.cert_classrel);
   16.44 +  gen_classrel (Logic.mk_classrel oo Axclass.cert_classrel);
   16.45  val classrel_cmd =
   16.46 -  gen_classrel (Logic.mk_classrel oo AxClass.read_classrel);
   16.47 +  gen_classrel (Logic.mk_classrel oo Axclass.read_classrel);
   16.48  
   16.49  end; (*local*)
   16.50  
   16.51 @@ -472,7 +472,7 @@
   16.52    let
   16.53      val Instantiation {params, ...} = Instantiation.get ctxt;
   16.54  
   16.55 -    val lookup_inst_param = AxClass.lookup_inst_param
   16.56 +    val lookup_inst_param = Axclass.lookup_inst_param
   16.57        (Sign.consts_of (Proof_Context.theory_of ctxt)) params;
   16.58      fun subst (c, ty) =
   16.59        (case lookup_inst_param (c, ty) of
   16.60 @@ -505,8 +505,8 @@
   16.61  (* target *)
   16.62  
   16.63  fun define_overloaded (c, U) v (b_def, rhs) =
   16.64 -  Local_Theory.background_theory_result (AxClass.declare_overloaded (c, U)
   16.65 -  ##>> AxClass.define_overloaded b_def (c, rhs))
   16.66 +  Local_Theory.background_theory_result (Axclass.declare_overloaded (c, U)
   16.67 +  ##>> Axclass.define_overloaded b_def (c, rhs))
   16.68    ##> (map_instantiation o apsnd) (filter_out (fn (_, (v', _)) => v' = v))
   16.69    ##> Local_Theory.map_contexts (K synchronize_inst_syntax);
   16.70  
   16.71 @@ -541,9 +541,9 @@
   16.72      val naming = Sign.naming_of thy;
   16.73  
   16.74      val _ = if null tycos then error "At least one arity must be given" else ();
   16.75 -    val class_params = these_params thy (filter (can (AxClass.get_info thy)) sort);
   16.76 +    val class_params = these_params thy (filter (can (Axclass.get_info thy)) sort);
   16.77      fun get_param tyco (param, (_, (c, ty))) =
   16.78 -      if can (AxClass.param_of_inst thy) (c, tyco)
   16.79 +      if can (Axclass.param_of_inst thy) (c, tyco)
   16.80        then NONE else SOME ((c, tyco),
   16.81          (param ^ "_" ^ Long_Name.base_name tyco, map_atyps (K (Type (tyco, map TFree vs))) ty));
   16.82      val params = map_product get_param tycos class_params |> map_filter I;
   16.83 @@ -559,7 +559,7 @@
   16.84      val improve_constraints = AList.lookup (op =)
   16.85        (map (fn (_, (class, (c, _))) => (c, [[class]])) class_params);
   16.86      fun resort_check ctxt ts = resort_terms ctxt algebra consts improve_constraints ts;
   16.87 -    val lookup_inst_param = AxClass.lookup_inst_param consts params;
   16.88 +    val lookup_inst_param = Axclass.lookup_inst_param consts params;
   16.89      fun improve (c, ty) =
   16.90        (case lookup_inst_param (c, ty) of
   16.91          SOME (_, ty') => if Sign.typ_instance thy (ty', ty) then SOME (ty, ty') else NONE
   16.92 @@ -593,7 +593,7 @@
   16.93      val (tycos, vs, sort) = (#arities o the_instantiation) lthy;
   16.94      val arities_proof = maps (fn tyco => Logic.mk_arities (tyco, map snd vs, sort)) tycos;
   16.95      fun after_qed' results =
   16.96 -      Local_Theory.background_theory (fold (AxClass.add_arity o Thm.varifyT_global) results)
   16.97 +      Local_Theory.background_theory (fold (Axclass.add_arity o Thm.varifyT_global) results)
   16.98        #> after_qed;
   16.99    in
  16.100      lthy
  16.101 @@ -630,7 +630,7 @@
  16.102      val sorts = map snd vs;
  16.103      val arities = maps (fn tyco => Logic.mk_arities (tyco, sorts, sort)) tycos;
  16.104      fun after_qed results =
  16.105 -      Proof_Context.background_theory ((fold o fold) AxClass.add_arity results);
  16.106 +      Proof_Context.background_theory ((fold o fold) Axclass.add_arity results);
  16.107    in
  16.108      thy
  16.109      |> Proof_Context.init_global
  16.110 @@ -645,7 +645,7 @@
  16.111      val thy = Thm.theory_of_thm st;
  16.112      val classes = Sign.all_classes thy;
  16.113      val class_trivs = map (Thm.class_triv thy) classes;
  16.114 -    val class_intros = map_filter (try (#intro o AxClass.get_info thy)) classes;
  16.115 +    val class_intros = map_filter (try (#intro o Axclass.get_info thy)) classes;
  16.116      val assm_intros = all_assm_intros thy;
  16.117    in
  16.118      Method.intros_tac (class_trivs @ class_intros @ assm_intros) facts st
    17.1 --- a/src/Pure/Isar/class_declaration.ML	Wed Apr 10 13:10:38 2013 +0200
    17.2 +++ b/src/Pure/Isar/class_declaration.ML	Wed Apr 10 15:30:19 2013 +0200
    17.3 @@ -90,7 +90,7 @@
    17.4            ((map_types o map_atyps) (K aT) prop), of_class_prop_concl));
    17.5      val sup_of_classes = map (snd o Class.rules thy) sups;
    17.6      val loc_axiom_intros = map Drule.export_without_context_open (Locale.axioms_of thy class);
    17.7 -    val axclass_intro = #intro (AxClass.get_info thy class);
    17.8 +    val axclass_intro = #intro (Axclass.get_info thy class);
    17.9      val base_sort_trivs = Thm.of_sort (Thm.ctyp_of thy aT, base_sort);
   17.10      val tac =
   17.11        REPEAT (SOMEGOAL
   17.12 @@ -289,13 +289,13 @@
   17.13        |> fst
   17.14        |> Option.map (Logic.unvarify_global o Logic.strip_imp_concl o Thm.prop_of);
   17.15      fun get_axiom thy =
   17.16 -      (case #axioms (AxClass.get_info thy class) of
   17.17 +      (case #axioms (Axclass.get_info thy class) of
   17.18           [] => NONE
   17.19        | [thm] => SOME thm);
   17.20    in
   17.21      thy
   17.22      |> add_consts class base_sort sups supparam_names global_syntax
   17.23 -    |-> (fn (param_map, params) => AxClass.define_class (bname, supsort)
   17.24 +    |-> (fn (param_map, params) => Axclass.define_class (bname, supsort)
   17.25            (map (fst o snd) params)
   17.26            [(Thm.empty_binding, Option.map (globalize param_map) raw_pred |> the_list)]
   17.27      #> snd
   17.28 @@ -346,7 +346,7 @@
   17.29        (case Named_Target.peek lthy of
   17.30           SOME {target, is_class = true, ...} => target
   17.31        | _ => error "Not in a class target");
   17.32 -    val (sub, sup) = AxClass.cert_classrel thy (proto_sub, proto_sup);
   17.33 +    val (sub, sup) = Axclass.cert_classrel thy (proto_sub, proto_sup);
   17.34  
   17.35      val expr = ([(sup, (("", false), Expression.Positional []))], []);
   17.36      val (([props], deps, export), goal_ctxt) =
    18.1 --- a/src/Pure/Isar/code.ML	Wed Apr 10 13:10:38 2013 +0200
    18.2 +++ b/src/Pure/Isar/code.ML	Wed Apr 10 15:30:19 2013 +0200
    18.3 @@ -107,7 +107,7 @@
    18.4  
    18.5  fun string_of_const thy c =
    18.6    let val ctxt = Proof_Context.init_global thy in
    18.7 -    case AxClass.inst_of_param thy c of
    18.8 +    case Axclass.inst_of_param thy c of
    18.9        SOME (c, tyco) =>
   18.10          Proof_Context.extern_const ctxt c ^ " " ^ enclose "[" "]"
   18.11            (Proof_Context.extern_type ctxt tyco)
   18.12 @@ -140,7 +140,7 @@
   18.13  
   18.14  fun check_unoverload thy (c, ty) =
   18.15    let
   18.16 -    val c' = AxClass.unoverload_const thy (c, ty);
   18.17 +    val c' = Axclass.unoverload_const thy (c, ty);
   18.18      val ty_decl = Sign.the_const_type thy c';
   18.19    in
   18.20      if typscheme_equiv (ty_decl, Logic.varifyT_global ty)
   18.21 @@ -375,7 +375,7 @@
   18.22  
   18.23  fun constrset_of_consts thy consts =
   18.24    let
   18.25 -    val _ = map (fn (c, _) => if (is_some o AxClass.class_of_param thy) c
   18.26 +    val _ = map (fn (c, _) => if (is_some o Axclass.class_of_param thy) c
   18.27        then error ("Is a class parameter: " ^ string_of_const thy c) else ()) consts;
   18.28      val raw_constructors = map (analyze_constructor thy) consts;
   18.29      val tyco = case distinct (op =) (map (fst o fst) raw_constructors)
   18.30 @@ -477,7 +477,7 @@
   18.31        else bad_thm "Free type variables on right hand side of equation";
   18.32      val (head, args) = strip_comb lhs;
   18.33      val (c, ty) = case head
   18.34 -     of Const (c_ty as (_, ty)) => (AxClass.unoverload_const thy c_ty, ty)
   18.35 +     of Const (c_ty as (_, ty)) => (Axclass.unoverload_const thy c_ty, ty)
   18.36        | _ => bad_thm "Equation not headed by constant";
   18.37      fun check _ (Abs _) = bad_thm "Abstraction on left hand side of equation"
   18.38        | check 0 (Var _) = ()
   18.39 @@ -485,7 +485,7 @@
   18.40        | check n (t1 $ t2) = (check (n+1) t1; check 0 t2)
   18.41        | check n (Const (c_ty as (c, ty))) =
   18.42            if allow_pats then let
   18.43 -            val c' = AxClass.unoverload_const thy c_ty
   18.44 +            val c' = Axclass.unoverload_const thy c_ty
   18.45            in if n = (length o binder_types) ty
   18.46              then if allow_consts orelse is_constr thy c'
   18.47                then ()
   18.48 @@ -495,7 +495,7 @@
   18.49      val _ = map (check 0) args;
   18.50      val _ = if allow_nonlinear orelse is_linear thm then ()
   18.51        else bad_thm "Duplicate variables on left hand side of equation";
   18.52 -    val _ = if (is_none o AxClass.class_of_param thy) c then ()
   18.53 +    val _ = if (is_none o Axclass.class_of_param thy) c then ()
   18.54        else bad_thm "Overloaded constant as head in equation";
   18.55      val _ = if not (is_constr thy c) then ()
   18.56        else bad_thm "Constructor as head in equation";
   18.57 @@ -557,13 +557,13 @@
   18.58  fun const_typ_eqn thy thm =
   18.59    let
   18.60      val (c, ty) = head_eqn thm;
   18.61 -    val c' = AxClass.unoverload_const thy (c, ty);
   18.62 +    val c' = Axclass.unoverload_const thy (c, ty);
   18.63        (*permissive wrt. to overloaded constants!*)
   18.64    in (c', ty) end;
   18.65  
   18.66  fun const_eqn thy = fst o const_typ_eqn thy;
   18.67  
   18.68 -fun const_abs_eqn thy = AxClass.unoverload_const thy o dest_Const o fst o strip_comb o snd
   18.69 +fun const_abs_eqn thy = Axclass.unoverload_const thy o dest_Const o fst o strip_comb o snd
   18.70    o dest_comb o fst o Logic.dest_equals o Thm.plain_prop_of;
   18.71  
   18.72  fun mk_proj tyco vs ty abs rep =
   18.73 @@ -629,14 +629,14 @@
   18.74  
   18.75  fun check_abstype_cert thy proto_thm =
   18.76    let
   18.77 -    val thm = (AxClass.unoverload thy o meta_rewrite thy) proto_thm;
   18.78 +    val thm = (Axclass.unoverload thy o meta_rewrite thy) proto_thm;
   18.79      val (lhs, rhs) = Logic.dest_equals (Thm.plain_prop_of thm)
   18.80        handle TERM _ => bad_thm "Not an equation"
   18.81             | THM _ => bad_thm "Not a proper equation";
   18.82      val ((abs, raw_ty), ((rep, rep_ty), param)) = (apsnd (apfst dest_Const o dest_comb)
   18.83          o apfst dest_Const o dest_comb) lhs
   18.84        handle TERM _ => bad_thm "Not an abstype certificate";
   18.85 -    val _ = pairself (fn c => if (is_some o AxClass.class_of_param thy) c
   18.86 +    val _ = pairself (fn c => if (is_some o Axclass.class_of_param thy) c
   18.87        then error ("Is a class parameter: " ^ string_of_const thy c) else ()) (abs, rep);
   18.88      val _ = check_decl_ty thy (abs, raw_ty);
   18.89      val _ = check_decl_ty thy (rep, rep_ty);
   18.90 @@ -714,7 +714,7 @@
   18.91    let
   18.92      val raw_ty = Logic.unvarifyT_global (const_typ thy c);
   18.93      val (vs, _) = typscheme thy (c, raw_ty);
   18.94 -    val sortargs = case AxClass.class_of_param thy c
   18.95 +    val sortargs = case Axclass.class_of_param thy c
   18.96       of SOME class => [[class]]
   18.97        | NONE => (case get_type_of_constr_or_abstr thy c
   18.98           of SOME (tyco, _) => (map snd o fst o the)
   18.99 @@ -840,12 +840,12 @@
  18.100        end;
  18.101  
  18.102  fun pretty_cert thy (cert as Equations _) =
  18.103 -      (map_filter (Option.map (Display.pretty_thm_global thy o AxClass.overload thy) o fst o snd)
  18.104 +      (map_filter (Option.map (Display.pretty_thm_global thy o Axclass.overload thy) o fst o snd)
  18.105           o snd o equations_of_cert thy) cert
  18.106    | pretty_cert thy (Projection (t, _)) =
  18.107        [Syntax.pretty_term_global thy (Logic.varify_types_global t)]
  18.108    | pretty_cert thy (Abstract (abs_thm, _)) =
  18.109 -      [(Display.pretty_thm_global thy o AxClass.overload thy o Thm.varifyT_global) abs_thm];
  18.110 +      [(Display.pretty_thm_global thy o Axclass.overload thy o Thm.varifyT_global) abs_thm];
  18.111  
  18.112  fun bare_thms_of_cert thy (cert as Equations _) =
  18.113        (map_filter (fn (_, (some_thm, proper)) => if proper then some_thm else NONE)
  18.114 @@ -881,7 +881,7 @@
  18.115    (map o apfst) (Thm.transfer thy)
  18.116    #> perhaps (perhaps_loop (perhaps_apply functrans))
  18.117    #> (map o apfst) (rewrite_eqn thy eqn_conv ss) 
  18.118 -  #> (map o apfst) (AxClass.unoverload thy)
  18.119 +  #> (map o apfst) (Axclass.unoverload thy)
  18.120    #> cert_of_eqns thy c;
  18.121  
  18.122  fun get_cert thy { functrans, ss } c =
  18.123 @@ -895,7 +895,7 @@
  18.124      | Abstr (abs_thm, tyco) => abs_thm
  18.125          |> Thm.transfer thy
  18.126          |> rewrite_eqn thy Conv.arg_conv ss
  18.127 -        |> AxClass.unoverload thy
  18.128 +        |> Axclass.unoverload thy
  18.129          |> cert_of_abs thy tyco c;
  18.130  
  18.131  
  18.132 @@ -1172,7 +1172,7 @@
  18.133          #> (map_cases o apfst) drop_outdated_cases)
  18.134    end;
  18.135  
  18.136 -fun unoverload_const_typ thy (c, ty) = (AxClass.unoverload_const thy (c, ty), ty);
  18.137 +fun unoverload_const_typ thy (c, ty) = (Axclass.unoverload_const thy (c, ty), ty);
  18.138  
  18.139  structure Datatype_Interpretation =
  18.140    Interpretation(type T = string * serial val eq = eq_snd (op =) : T * T -> bool);
    19.1 --- a/src/Pure/Isar/isar_syn.ML	Wed Apr 10 13:10:38 2013 +0200
    19.2 +++ b/src/Pure/Isar/isar_syn.ML	Wed Apr 10 15:30:19 2013 +0200
    19.3 @@ -79,13 +79,13 @@
    19.4    Outer_Syntax.command @{command_spec "classes"} "declare type classes"
    19.5      (Scan.repeat1 (Parse.binding -- Scan.optional ((@{keyword "\<subseteq>"} || @{keyword "<"}) |--
    19.6          Parse.!!! (Parse.list1 Parse.class)) [])
    19.7 -      >> (Toplevel.theory o fold AxClass.axiomatize_class_cmd));
    19.8 +      >> (Toplevel.theory o fold Axclass.axiomatize_class_cmd));
    19.9  
   19.10  val _ =
   19.11    Outer_Syntax.command @{command_spec "classrel"} "state inclusion of type classes (axiomatic!)"
   19.12      (Parse.and_list1 (Parse.class -- ((@{keyword "\<subseteq>"} || @{keyword "<"})
   19.13          |-- Parse.!!! Parse.class))
   19.14 -    >> (Toplevel.theory o AxClass.axiomatize_classrel_cmd));
   19.15 +    >> (Toplevel.theory o Axclass.axiomatize_classrel_cmd));
   19.16  
   19.17  val _ =
   19.18    Outer_Syntax.local_theory @{command_spec "default_sort"}
   19.19 @@ -113,7 +113,7 @@
   19.20  
   19.21  val _ =
   19.22    Outer_Syntax.command @{command_spec "arities"} "state type arities (axiomatic!)"
   19.23 -    (Scan.repeat1 Parse.arity >> (Toplevel.theory o fold AxClass.axiomatize_arity_cmd));
   19.24 +    (Scan.repeat1 Parse.arity >> (Toplevel.theory o fold Axclass.axiomatize_arity_cmd));
   19.25  
   19.26  
   19.27  (* consts and syntax *)
    20.1 --- a/src/Pure/Isar/typedecl.ML	Wed Apr 10 13:10:38 2013 +0200
    20.2 +++ b/src/Pure/Isar/typedecl.ML	Wed Apr 10 15:30:19 2013 +0200
    20.3 @@ -29,7 +29,7 @@
    20.4  fun object_logic_arity name thy =
    20.5    (case Object_Logic.get_base_sort thy of
    20.6      NONE => thy
    20.7 -  | SOME S => AxClass.axiomatize_arity (name, replicate (Sign.arity_number thy name) S, S) thy);
    20.8 +  | SOME S => Axclass.axiomatize_arity (name, replicate (Sign.arity_number thy name) S, S) thy);
    20.9  
   20.10  fun basic_decl decl (b, n, mx) lthy =
   20.11    let val name = Local_Theory.full_name lthy b in
    21.1 --- a/src/Pure/axclass.ML	Wed Apr 10 13:10:38 2013 +0200
    21.2 +++ b/src/Pure/axclass.ML	Wed Apr 10 15:30:19 2013 +0200
    21.3 @@ -5,7 +5,7 @@
    21.4  parameters.  Proven class relations and type arities.
    21.5  *)
    21.6  
    21.7 -signature AX_CLASS =
    21.8 +signature AXCLASS =
    21.9  sig
   21.10    type info = {def: thm, intro: thm, axioms: thm list, params: (string * typ) list}
   21.11    val get_info: theory -> class -> info
   21.12 @@ -38,7 +38,7 @@
   21.13    val axiomatize_arity_cmd: xstring * string list * string -> theory -> theory
   21.14  end;
   21.15  
   21.16 -structure AxClass: AX_CLASS =
   21.17 +structure Axclass: AXCLASS =
   21.18  struct
   21.19  
   21.20  (** theory data **)
    22.1 --- a/src/Tools/Code/code_preproc.ML	Wed Apr 10 13:10:38 2013 +0200
    22.2 +++ b/src/Tools/Code/code_preproc.ML	Wed Apr 10 15:30:19 2013 +0200
    22.3 @@ -143,7 +143,7 @@
    22.4      val pre = (Simplifier.global_context thy o #pre o the_thmproc) thy;
    22.5    in
    22.6      Simplifier.rewrite pre
    22.7 -    #> trans_conv_rule (AxClass.unoverload_conv thy)
    22.8 +    #> trans_conv_rule (Axclass.unoverload_conv thy)
    22.9    end;
   22.10  
   22.11  fun preprocess_term thy = term_of_conv_resubst thy (preprocess_conv thy);
   22.12 @@ -152,7 +152,7 @@
   22.13    let
   22.14      val post = (Simplifier.global_context thy o #post o the_thmproc) thy;
   22.15    in
   22.16 -    AxClass.overload_conv thy
   22.17 +    Axclass.overload_conv thy
   22.18      #> trans_conv_rule (Simplifier.rewrite post)
   22.19    end;
   22.20  
   22.21 @@ -213,14 +213,14 @@
   22.22  
   22.23  (* auxiliary *)
   22.24  
   22.25 -fun is_proper_class thy = can (AxClass.get_info thy);
   22.26 +fun is_proper_class thy = can (Axclass.get_info thy);
   22.27  
   22.28  fun complete_proper_sort thy =
   22.29    Sign.complete_sort thy #> filter (is_proper_class thy);
   22.30  
   22.31  fun inst_params thy tyco =
   22.32 -  map (fn (c, _) => AxClass.param_of_inst thy (c, tyco))
   22.33 -    o maps (#params o AxClass.get_info thy);
   22.34 +  map (fn (c, _) => Axclass.param_of_inst thy (c, tyco))
   22.35 +    o maps (#params o Axclass.get_info thy);
   22.36  
   22.37  
   22.38  (* data structures *)
    23.1 --- a/src/Tools/Code/code_target.ML	Wed Apr 10 13:10:38 2013 +0200
    23.2 +++ b/src/Tools/Code/code_target.ML	Wed Apr 10 15:30:19 2013 +0200
    23.3 @@ -544,7 +544,7 @@
    23.4  
    23.5  fun cert_class thy class =
    23.6    let
    23.7 -    val _ = AxClass.get_info thy class;
    23.8 +    val _ = Axclass.get_info thy class;
    23.9    in class end;
   23.10  
   23.11  fun read_class thy = cert_class thy o Sign.intern_class thy;
    24.1 --- a/src/Tools/Code/code_thingol.ML	Wed Apr 10 13:10:38 2013 +0200
    24.2 +++ b/src/Tools/Code/code_thingol.ML	Wed Apr 10 15:30:19 2013 +0200
    24.3 @@ -269,10 +269,10 @@
    24.4  local
    24.5    fun thyname_of_type thy = #theory_name o Name_Space.the_entry (Sign.type_space thy);
    24.6    fun thyname_of_class thy = #theory_name o Name_Space.the_entry (Sign.class_space thy);
    24.7 -  fun thyname_of_instance thy inst = case AxClass.thynames_of_arity thy inst
    24.8 +  fun thyname_of_instance thy inst = case Axclass.thynames_of_arity thy inst
    24.9     of [] => error ("No such instance: " ^ quote (snd inst ^ " :: " ^ fst inst))
   24.10      | thyname :: _ => thyname;
   24.11 -  fun thyname_of_const thy c = case AxClass.class_of_param thy c
   24.12 +  fun thyname_of_const thy c = case Axclass.class_of_param thy c
   24.13     of SOME class => thyname_of_class thy class
   24.14      | NONE => (case Code.get_type_of_constr_or_abstr thy c
   24.15         of SOME (tyco, _) => thyname_of_type thy tyco
   24.16 @@ -662,14 +662,14 @@
   24.17        end;
   24.18      val stmt_const = case Code.get_type_of_constr_or_abstr thy c
   24.19       of SOME (tyco, _) => stmt_datatypecons tyco
   24.20 -      | NONE => (case AxClass.class_of_param thy c
   24.21 +      | NONE => (case Axclass.class_of_param thy c
   24.22           of SOME class => stmt_classparam class
   24.23            | NONE => stmt_fun (Code_Preproc.cert eqngr c))
   24.24    in ensure_stmt lookup_const (declare_const thy) stmt_const c end
   24.25  and ensure_class thy (algbr as (_, algebra)) eqngr permissive class =
   24.26    let
   24.27      val super_classes = (Sorts.minimize_sort algebra o Sorts.super_classes algebra) class;
   24.28 -    val cs = #params (AxClass.get_info thy class);
   24.29 +    val cs = #params (Axclass.get_info thy class);
   24.30      val stmt_class =
   24.31        fold_map (fn super_class => ensure_class thy algbr eqngr permissive super_class
   24.32          ##>> ensure_classrel thy algbr eqngr permissive (class, super_class)) super_classes
   24.33 @@ -687,7 +687,7 @@
   24.34  and ensure_inst thy (algbr as (_, algebra)) eqngr permissive (class, tyco) =
   24.35    let
   24.36      val super_classes = (Sorts.minimize_sort algebra o Sorts.super_classes algebra) class;
   24.37 -    val these_class_params = these o try (#params o AxClass.get_info thy);
   24.38 +    val these_class_params = these o try (#params o Axclass.get_info thy);
   24.39      val class_params = these_class_params class;
   24.40      val superclass_params = maps these_class_params
   24.41        ((Sorts.complete_sort algebra o Sorts.super_classes algebra) class);
   24.42 @@ -706,7 +706,7 @@
   24.43      fun translate_classparam_instance (c, ty) =
   24.44        let
   24.45          val raw_const = Const (c, map_type_tfree (K arity_typ') ty);
   24.46 -        val thm = AxClass.unoverload_conv thy (Thm.cterm_of thy raw_const);
   24.47 +        val thm = Axclass.unoverload_conv thy (Thm.cterm_of thy raw_const);
   24.48          val const = (apsnd Logic.unvarifyT_global o dest_Const o snd
   24.49            o Logic.dest_equals o Thm.prop_of) thm;
   24.50        in
    25.1 --- a/src/Tools/nbe.ML	Wed Apr 10 13:10:38 2013 +0200
    25.2 +++ b/src/Tools/nbe.ML	Wed Apr 10 15:30:19 2013 +0200
    25.3 @@ -56,7 +56,7 @@
    25.4       of SOME T_class => T_class
    25.5        | _ => error ("Bad certificate: " ^ Display.string_of_thm_global thy thm);
    25.6      val tvar = case try Term.dest_TVar T
    25.7 -     of SOME (tvar as (_, sort)) => if null (filter (can (AxClass.get_info thy)) sort)
    25.8 +     of SOME (tvar as (_, sort)) => if null (filter (can (Axclass.get_info thy)) sort)
    25.9            then tvar
   25.10            else error ("Bad sort: " ^ Display.string_of_thm_global thy thm)
   25.11        | _ => error ("Bad type: " ^ Display.string_of_thm_global thy thm);
   25.12 @@ -65,11 +65,11 @@
   25.13      val lhs_rhs = case try Logic.dest_equals eqn
   25.14       of SOME lhs_rhs => lhs_rhs
   25.15        | _ => error ("Not an equation: " ^ Syntax.string_of_term_global thy eqn);
   25.16 -    val c_c' = case try (pairself (AxClass.unoverload_const thy o dest_Const)) lhs_rhs
   25.17 +    val c_c' = case try (pairself (Axclass.unoverload_const thy o dest_Const)) lhs_rhs
   25.18       of SOME c_c' => c_c'
   25.19        | _ => error ("Not an equation with two constants: "
   25.20            ^ Syntax.string_of_term_global thy eqn);
   25.21 -    val _ = if the_list (AxClass.class_of_param thy (snd c_c')) = [class] then ()
   25.22 +    val _ = if the_list (Axclass.class_of_param thy (snd c_c')) = [class] then ()
   25.23        else error ("Inconsistent class: " ^ Display.string_of_thm_global thy thm);
   25.24    in Triv_Class_Data.map (AList.update (op =) (class, thm)) thy end;
   25.25