--- a/src/Doc/more_antiquote.ML Wed Apr 10 13:10:38 2013 +0200
+++ b/src/Doc/more_antiquote.ML Wed Apr 10 15:30:19 2013 +0200
@@ -36,7 +36,7 @@
|> Code.equations_of_cert thy
|> snd
|> map_filter (fn (_, (some_thm, proper)) => if proper then some_thm else NONE)
- |> map (holize o no_vars ctxt o AxClass.overload thy);
+ |> map (holize o no_vars ctxt o Axclass.overload thy);
in Thy_Output.output ctxt (Thy_Output.maybe_pretty_source pretty_thm ctxt src thms) end;
in
--- a/src/HOL/HOLCF/Tools/Domain/domain.ML Wed Apr 10 13:10:38 2013 +0200
+++ b/src/HOL/HOLCF/Tools/Domain/domain.ML Wed Apr 10 15:30:19 2013 +0200
@@ -44,7 +44,7 @@
fun add_arity ((b, sorts, mx), sort) thy : theory =
thy
|> Sign.add_types_global [(b, length sorts, mx)]
- |> AxClass.axiomatize_arity (Sign.full_name thy b, sorts, sort)
+ |> Axclass.axiomatize_arity (Sign.full_name thy b, sorts, sort)
fun gen_add_domain
(prep_sort : theory -> 'a -> sort)
--- a/src/HOL/HOLCF/Tools/Domain/domain_axioms.ML Wed Apr 10 13:10:38 2013 +0200
+++ b/src/HOL/HOLCF/Tools/Domain/domain_axioms.ML Wed Apr 10 15:30:19 2013 +0200
@@ -104,7 +104,7 @@
fun thy_arity (_, _, (lhsT, _)) =
let val (dname, tvars) = dest_Type lhsT
in (dname, map (snd o dest_TFree) tvars, @{sort pcpo}) end
- val thy = fold (AxClass.axiomatize_arity o thy_arity) dom_eqns thy
+ val thy = fold (Axclass.axiomatize_arity o thy_arity) dom_eqns thy
(* declare and axiomatize abs/rep *)
val (iso_infos, thy) =
--- a/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML Wed Apr 10 13:10:38 2013 +0200
+++ b/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML Wed Apr 10 15:30:19 2013 +0200
@@ -427,7 +427,7 @@
fun arity (vs, tbind, _, _, _) =
(Sign.full_name thy tbind, map the_sort vs, @{sort "domain"})
in
- fold AxClass.axiomatize_arity (map arity doms) tmp_thy
+ fold Axclass.axiomatize_arity (map arity doms) tmp_thy
end
(* check bifiniteness of right-hand sides *)
--- a/src/HOL/HOLCF/Tools/cpodef.ML Wed Apr 10 13:10:38 2013 +0200
+++ b/src/HOL/HOLCF/Tools/cpodef.ML Wed Apr 10 15:30:19 2013 +0200
@@ -74,7 +74,7 @@
val (full_tname, Ts) = dest_Type newT
val lhs_sorts = map (snd o dest_TFree) Ts
val tac = Tactic.rtac (@{thm typedef_cpo} OF cpo_thms) 1
- val thy = AxClass.prove_arity (full_tname, lhs_sorts, @{sort cpo}) (K tac) thy
+ val thy = Axclass.prove_arity (full_tname, lhs_sorts, @{sort cpo}) (K tac) thy
(* transfer thms so that they will know about the new cpo instance *)
val cpo_thms' = map (Thm.transfer thy) cpo_thms
fun make thm = Drule.zero_var_indexes (thm OF cpo_thms')
@@ -113,7 +113,7 @@
val (full_tname, Ts) = dest_Type newT
val lhs_sorts = map (snd o dest_TFree) Ts
val tac = Tactic.rtac (@{thm typedef_pcpo} OF pcpo_thms) 1
- val thy = AxClass.prove_arity (full_tname, lhs_sorts, @{sort pcpo}) (K tac) thy
+ val thy = Axclass.prove_arity (full_tname, lhs_sorts, @{sort pcpo}) (K tac) thy
val pcpo_thms' = map (Thm.transfer thy) pcpo_thms
fun make thm = Drule.zero_var_indexes (thm OF pcpo_thms')
val Rep_strict = make @{thm typedef_Rep_strict}
--- a/src/HOL/Library/refute.ML Wed Apr 10 13:10:38 2013 +0200
+++ b/src/HOL/Library/refute.ML Wed Apr 10 15:30:19 2013 +0200
@@ -695,7 +695,7 @@
val superclasses = distinct (op =) superclasses
val class_axioms = maps (fn class => map (fn ax =>
("<" ^ class ^ ">", Thm.prop_of ax))
- (#axioms (AxClass.get_info thy class) handle ERROR _ => []))
+ (#axioms (Axclass.get_info thy class) handle ERROR _ => []))
superclasses
(* replace the (at most one) schematic type variable in each axiom *)
(* by the actual type 'T' *)
--- a/src/HOL/Nominal/nominal_atoms.ML Wed Apr 10 13:10:38 2013 +0200
+++ b/src/HOL/Nominal/nominal_atoms.ML Wed Apr 10 15:30:19 2013 +0200
@@ -311,7 +311,7 @@
(HOLogic.mk_Trueprop (cprm_eq $ pi1 $ pi2),
HOLogic.mk_Trueprop (HOLogic.mk_eq (cperm $ pi1 $ x, cperm $ pi2 $ x)));
in
- AxClass.define_class (Binding.name cl_name, ["HOL.type"]) []
+ Axclass.define_class (Binding.name cl_name, ["HOL.type"]) []
[((Binding.name (cl_name ^ "1"), [Simplifier.simp_add]), [axiom1]),
((Binding.name (cl_name ^ "2"), []), [axiom2]),
((Binding.name (cl_name ^ "3"), []), [axiom3])] thy
@@ -360,7 +360,7 @@
val axiom1 = HOLogic.mk_Trueprop (cfinite $ (csupp $ x));
in
- AxClass.define_class (Binding.name cl_name, [pt_name]) []
+ Axclass.define_class (Binding.name cl_name, [pt_name]) []
[((Binding.name (cl_name ^ "1"), []), [axiom1])] thy
end) ak_names_types thy8;
@@ -410,7 +410,7 @@
(HOLogic.mk_eq (cperm1 $ pi1 $ (cperm2 $ pi2 $ x),
cperm2 $ (cperm3 $ pi1 $ pi2) $ (cperm1 $ pi1 $ x)));
in
- AxClass.define_class (Binding.name cl_name, ["HOL.type"]) []
+ Axclass.define_class (Binding.name cl_name, ["HOL.type"]) []
[((Binding.name (cl_name ^ "1"), []), [ax1])] thy'
end) ak_names_types thy) ak_names_types thy12;
@@ -517,7 +517,7 @@
in
thy'
- |> AxClass.prove_arity (qu_name,[],[cls_name])
+ |> Axclass.prove_arity (qu_name,[],[cls_name])
(fn _ => if ak_name = ak_name' then proof1 else proof2)
end) ak_names thy) ak_names thy12d;
@@ -551,15 +551,15 @@
val pt_thm_unit = pt_unit_inst;
in
thy
- |> AxClass.prove_arity ("fun",[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_fun)
- |> AxClass.prove_arity (@{type_name Set.set},[[cls_name]],[cls_name]) (pt_proof pt_thm_set)
- |> AxClass.prove_arity ("Nominal.noption",[[cls_name]],[cls_name]) (pt_proof pt_thm_noptn)
- |> AxClass.prove_arity ("Option.option",[[cls_name]],[cls_name]) (pt_proof pt_thm_optn)
- |> AxClass.prove_arity ("List.list",[[cls_name]],[cls_name]) (pt_proof pt_thm_list)
- |> AxClass.prove_arity (@{type_name Product_Type.prod},[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_prod)
- |> AxClass.prove_arity ("Nominal.nprod",[[cls_name],[cls_name]],[cls_name])
+ |> Axclass.prove_arity ("fun",[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_fun)
+ |> Axclass.prove_arity (@{type_name Set.set},[[cls_name]],[cls_name]) (pt_proof pt_thm_set)
+ |> Axclass.prove_arity ("Nominal.noption",[[cls_name]],[cls_name]) (pt_proof pt_thm_noptn)
+ |> Axclass.prove_arity ("Option.option",[[cls_name]],[cls_name]) (pt_proof pt_thm_optn)
+ |> Axclass.prove_arity ("List.list",[[cls_name]],[cls_name]) (pt_proof pt_thm_list)
+ |> Axclass.prove_arity (@{type_name Product_Type.prod},[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_prod)
+ |> Axclass.prove_arity ("Nominal.nprod",[[cls_name],[cls_name]],[cls_name])
(pt_proof pt_thm_nprod)
- |> AxClass.prove_arity ("Product_Type.unit",[],[cls_name]) (pt_proof pt_thm_unit)
+ |> Axclass.prove_arity ("Product_Type.unit",[],[cls_name]) (pt_proof pt_thm_unit)
end) ak_names thy13;
(******** fs_<ak> class instances ********)
@@ -592,7 +592,7 @@
val simp_s = HOL_basic_ss addsimps [dj_inst RS dj_supp, finite_emptyI];
in EVERY [Class.intro_classes_tac [], asm_simp_tac simp_s 1] end)
in
- AxClass.prove_arity (qu_name,[],[qu_class]) (fn _ => proof) thy'
+ Axclass.prove_arity (qu_name,[],[qu_class]) (fn _ => proof) thy'
end) ak_names thy) ak_names thy18;
(* shows that *)
@@ -616,12 +616,12 @@
val fs_thm_optn = fs_inst RS fs_option_inst;
in
thy
- |> AxClass.prove_arity ("Product_Type.unit",[],[cls_name]) (fs_proof fs_thm_unit)
- |> AxClass.prove_arity (@{type_name Product_Type.prod},[[cls_name],[cls_name]],[cls_name]) (fs_proof fs_thm_prod)
- |> AxClass.prove_arity ("Nominal.nprod",[[cls_name],[cls_name]],[cls_name])
+ |> Axclass.prove_arity ("Product_Type.unit",[],[cls_name]) (fs_proof fs_thm_unit)
+ |> Axclass.prove_arity (@{type_name Product_Type.prod},[[cls_name],[cls_name]],[cls_name]) (fs_proof fs_thm_prod)
+ |> Axclass.prove_arity ("Nominal.nprod",[[cls_name],[cls_name]],[cls_name])
(fs_proof fs_thm_nprod)
- |> AxClass.prove_arity ("List.list",[[cls_name]],[cls_name]) (fs_proof fs_thm_list)
- |> AxClass.prove_arity ("Option.option",[[cls_name]],[cls_name]) (fs_proof fs_thm_optn)
+ |> Axclass.prove_arity ("List.list",[[cls_name]],[cls_name]) (fs_proof fs_thm_list)
+ |> Axclass.prove_arity ("Option.option",[[cls_name]],[cls_name]) (fs_proof fs_thm_optn)
end) ak_names thy20;
(******** cp_<ak>_<ai> class instances ********)
@@ -669,7 +669,7 @@
EVERY [Class.intro_classes_tac [], simp_tac simp_s 1]
end))
in
- AxClass.prove_arity (name,[],[cls_name]) (fn _ => proof) thy''
+ Axclass.prove_arity (name,[],[cls_name]) (fn _ => proof) thy''
end) ak_names thy') ak_names thy) ak_names thy24;
(* shows that *)
@@ -700,13 +700,13 @@
val cp_thm_set = cp_inst RS cp_set_inst;
in
thy'
- |> AxClass.prove_arity ("Product_Type.unit",[],[cls_name]) (cp_proof cp_thm_unit)
- |> AxClass.prove_arity (@{type_name Product_Type.prod}, [[cls_name],[cls_name]],[cls_name]) (cp_proof cp_thm_prod)
- |> AxClass.prove_arity ("List.list",[[cls_name]],[cls_name]) (cp_proof cp_thm_list)
- |> AxClass.prove_arity ("fun",[[cls_name],[cls_name]],[cls_name]) (cp_proof cp_thm_fun)
- |> AxClass.prove_arity ("Option.option",[[cls_name]],[cls_name]) (cp_proof cp_thm_optn)
- |> AxClass.prove_arity ("Nominal.noption",[[cls_name]],[cls_name]) (cp_proof cp_thm_noptn)
- |> AxClass.prove_arity (@{type_name Set.set},[[cls_name]],[cls_name]) (cp_proof cp_thm_set)
+ |> Axclass.prove_arity ("Product_Type.unit",[],[cls_name]) (cp_proof cp_thm_unit)
+ |> Axclass.prove_arity (@{type_name Product_Type.prod}, [[cls_name],[cls_name]],[cls_name]) (cp_proof cp_thm_prod)
+ |> Axclass.prove_arity ("List.list",[[cls_name]],[cls_name]) (cp_proof cp_thm_list)
+ |> Axclass.prove_arity ("fun",[[cls_name],[cls_name]],[cls_name]) (cp_proof cp_thm_fun)
+ |> Axclass.prove_arity ("Option.option",[[cls_name]],[cls_name]) (cp_proof cp_thm_optn)
+ |> Axclass.prove_arity ("Nominal.noption",[[cls_name]],[cls_name]) (cp_proof cp_thm_noptn)
+ |> Axclass.prove_arity (@{type_name Set.set},[[cls_name]],[cls_name]) (cp_proof cp_thm_set)
end) ak_names thy) ak_names thy25;
(* show that discrete nominal types are permutation types, finitely *)
@@ -722,7 +722,7 @@
val simp_s = HOL_basic_ss addsimps [Simpdata.mk_eq defn];
val proof = EVERY [Class.intro_classes_tac [], REPEAT (asm_simp_tac simp_s 1)];
in
- AxClass.prove_arity (discrete_ty, [], [qu_class]) (fn _ => proof) thy
+ Axclass.prove_arity (discrete_ty, [], [qu_class]) (fn _ => proof) thy
end) ak_names;
fun discrete_fs_inst discrete_ty defn =
@@ -733,7 +733,7 @@
val simp_s = HOL_ss addsimps [supp_def, Collect_const, finite_emptyI, Simpdata.mk_eq defn];
val proof = EVERY [Class.intro_classes_tac [], asm_simp_tac simp_s 1];
in
- AxClass.prove_arity (discrete_ty, [], [qu_class]) (fn _ => proof) thy
+ Axclass.prove_arity (discrete_ty, [], [qu_class]) (fn _ => proof) thy
end) ak_names;
fun discrete_cp_inst discrete_ty defn =
@@ -744,7 +744,7 @@
val simp_s = HOL_ss addsimps [Simpdata.mk_eq defn];
val proof = EVERY [Class.intro_classes_tac [], asm_simp_tac simp_s 1];
in
- AxClass.prove_arity (discrete_ty, [], [qu_class]) (fn _ => proof) thy
+ Axclass.prove_arity (discrete_ty, [], [qu_class]) (fn _ => proof) thy
end) ak_names)) ak_names;
in
--- a/src/HOL/Nominal/nominal_datatype.ML Wed Apr 10 13:10:38 2013 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML Wed Apr 10 15:30:19 2013 +0200
@@ -425,7 +425,7 @@
(fn {context = ctxt, ...} => EVERY [Datatype_Aux.ind_tac induct perm_indnames 1,
ALLGOALS (asm_full_simp_tac (simps ctxt))]))
in
- fold (fn (s, tvs) => fn thy => AxClass.prove_arity
+ fold (fn (s, tvs) => fn thy => Axclass.prove_arity
(s, map (inter_sort thy sort o snd) tvs, [cp_class])
(fn _ => Class.intro_classes_tac [] THEN ALLGOALS (resolve_tac thms)) thy)
(full_new_type_names' ~~ tyvars) thy
@@ -437,7 +437,7 @@
fold (fn atom => fn thy =>
let val pt_name = pt_class_of thy atom
in
- fold (fn (s, tvs) => fn thy => AxClass.prove_arity
+ fold (fn (s, tvs) => fn thy => Axclass.prove_arity
(s, map (inter_sort thy [pt_name] o snd) tvs, [pt_name])
(fn _ => EVERY
[Class.intro_classes_tac [],
@@ -618,7 +618,7 @@
val pt_class = pt_class_of thy atom;
val sort = Sign.minimize_sort thy (Sign.certify_sort thy
(pt_class :: map (cp_class_of thy atom) (remove (op =) atom dt_atoms)))
- in AxClass.prove_arity
+ in Axclass.prove_arity
(Sign.intern_type thy name,
map (inter_sort thy sort o snd) tvs, [pt_class])
(fn ctxt => EVERY [Class.intro_classes_tac [],
@@ -648,7 +648,7 @@
val cp1' = cp_inst_of thy atom1 atom2 RS cp1
in fold (fn ((((((Abs_inverse, Rep),
perm_def), name), tvs), perm_closed1), perm_closed2) => fn thy =>
- AxClass.prove_arity
+ Axclass.prove_arity
(Sign.intern_type thy name,
map (inter_sort thy sort o snd) tvs, [cp_class])
(fn ctxt => EVERY [Class.intro_classes_tac [],
@@ -1105,7 +1105,7 @@
let
val class = fs_class_of thy atom;
val sort = Sign.minimize_sort thy (Sign.certify_sort thy (class :: pt_cp_sort));
- in fold (fn Type (s, Ts) => AxClass.prove_arity
+ in fold (fn Type (s, Ts) => Axclass.prove_arity
(s, map (inter_sort thy sort o snd o dest_TFree) Ts, [class])
(fn _ => Class.intro_classes_tac [] THEN resolve_tac ths 1)) newTs thy
end) (atoms ~~ finite_supp_thms) ||>
--- a/src/HOL/Tools/Datatype/datatype_codegen.ML Wed Apr 10 13:10:38 2013 +0200
+++ b/src/HOL/Tools/Datatype/datatype_codegen.ML Wed Apr 10 15:30:19 2013 +0200
@@ -19,7 +19,7 @@
fun mk_constr_consts thy vs tyco cos =
let
val cs = map (fn (c, tys) => (c, tys ---> Type (tyco, map TFree vs))) cos;
- val cs' = map (fn c_ty as (_, ty) => (AxClass.unoverload_const thy c_ty, ty)) cs;
+ val cs' = map (fn c_ty as (_, ty) => (Axclass.unoverload_const thy c_ty, ty)) cs;
in
if is_some (try (Code.constrset_of_consts thy) cs')
then SOME cs
@@ -54,7 +54,7 @@
|> Raw_Simplifier.rewrite_rule [Thm.symmetric (Thm.assume asm)]
|> Thm.implies_intr asm
|> Thm.generalize ([], params) 0
- |> AxClass.unoverload thy
+ |> Axclass.unoverload thy
|> Thm.varifyT_global
end;
--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Wed Apr 10 13:10:38 2013 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Wed Apr 10 15:30:19 2013 +0200
@@ -1028,7 +1028,7 @@
let
val supers = Sign.complete_sort thy S
val class_axioms =
- maps (fn class => map prop_of (AxClass.get_info thy class |> #axioms
+ maps (fn class => map prop_of (Axclass.get_info thy class |> #axioms
handle ERROR _ => [])) supers
val monomorphic_class_axioms =
map (fn t => case Term.add_tvars t [] of
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Wed Apr 10 13:10:38 2013 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Wed Apr 10 15:30:19 2013 +0200
@@ -36,7 +36,7 @@
^ (space_implode "\n" (map (Display.string_of_thm_global thy) thms)) ^ "\n") specs
|> space_implode "\n" |> tracing
else ()
-fun overload_const thy s = the_default s (Option.map fst (AxClass.inst_of_param thy s))
+fun overload_const thy s = the_default s (Option.map fst (Axclass.inst_of_param thy s))
fun map_specs f specs =
map (fn (s, ths) => (s, f ths)) specs
@@ -109,7 +109,7 @@
val intross5 = map_specs (map (remove_equalities thy2)) intross4
val _ = print_intross options thy2 "After removing equality premises:" intross5
val intross6 =
- map (fn (s, ths) => (overload_const thy2 s, map (AxClass.overload thy2) ths)) intross5
+ map (fn (s, ths) => (overload_const thy2 s, map (Axclass.overload thy2) ths)) intross5
val intross7 = map_specs (map (expand_tuples thy2)) intross6
val intross8 = map_specs (map (eta_contract_ho_arguments thy2)) intross7
val _ = case !intro_hook of NONE => () | SOME f => (map_specs (map (f thy2)) intross8; ())
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Wed Apr 10 13:10:38 2013 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Wed Apr 10 15:30:19 2013 +0200
@@ -189,7 +189,7 @@
fun get_specification options thy t =
let
(*val (c, T) = dest_Const t
- val t = Const (AxClass.unoverload_const thy (c, T), T)*)
+ val t = Const (Axclass.unoverload_const thy (c, T), T)*)
val _ = if show_steps options then
tracing ("getting specification of " ^ Syntax.string_of_term_global thy t ^
" with type " ^ Syntax.string_of_typ_global thy (fastype_of t))
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Wed Apr 10 13:10:38 2013 +0200
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Wed Apr 10 15:30:19 2013 +0200
@@ -93,7 +93,7 @@
val ty = Type (tyco, map TFree vs);
val cs = (map o apsnd o apsnd o map o map_atyps)
(fn TFree (v, _) => TFree (v, (the o AList.lookup (op =) vs) v)) raw_cs;
- val const = AxClass.param_of_inst thy (@{const_name partial_term_of}, tyco);
+ val const = Axclass.param_of_inst thy (@{const_name partial_term_of}, tyco);
val var_insts =
map (SOME o Thm.cterm_of thy o Logic.unvarify_types_global o Logic.varify_global)
[Free ("ty", Term.itselfT ty), @{term "Quickcheck_Narrowing.Narrowing_variable p tt"},
--- a/src/HOL/Tools/code_evaluation.ML Wed Apr 10 13:10:38 2013 +0200
+++ b/src/HOL/Tools/code_evaluation.ML Wed Apr 10 15:30:19 2013 +0200
@@ -78,7 +78,7 @@
val ty = Type (tyco, map TFree vs);
val cs = (map o apsnd o apsnd o map o map_atyps)
(fn TFree (v, _) => TFree (v, (the o AList.lookup (op =) vs) v)) raw_cs;
- val const = AxClass.param_of_inst thy (@{const_name term_of}, tyco);
+ val const = Axclass.param_of_inst thy (@{const_name term_of}, tyco);
val eqs = map (mk_term_of_eq thy ty) cs;
in
thy
@@ -115,7 +115,7 @@
val ty = Type (tyco, map TFree vs);
val ty_rep = map_atyps
(fn TFree (v, _) => TFree (v, (the o AList.lookup (op =) vs) v)) raw_ty_rep;
- val const = AxClass.param_of_inst thy (@{const_name term_of}, tyco);
+ val const = Axclass.param_of_inst thy (@{const_name term_of}, tyco);
val eq = mk_abs_term_of_eq thy ty abs ty_rep proj;
in
thy
@@ -169,7 +169,7 @@
fun mk_term_of t = HOLogic.mk_term_of (fastype_of t) t;
-fun term_of_const_for thy = AxClass.unoverload_const thy o dest_Const o HOLogic.term_of_const;
+fun term_of_const_for thy = Axclass.unoverload_const thy o dest_Const o HOLogic.term_of_const;
fun gen_dynamic_value dynamic_value thy t =
dynamic_value cookie thy NONE I (mk_term_of t) [];
@@ -204,7 +204,7 @@
fun static_conv thy consts Ts =
let
val eqs = "==" :: @{const_name HOL.eq} ::
- map (fn T => AxClass.unoverload_const thy (@{const_name HOL.equal}, T)) Ts;
+ map (fn T => Axclass.unoverload_const thy (@{const_name HOL.equal}, T)) Ts;
(*assumes particular code equations for "==" etc.*)
in
certify_eval thy (static_value thy consts Ts)
--- a/src/HOL/Tools/record.ML Wed Apr 10 13:10:38 2013 +0200
+++ b/src/HOL/Tools/record.ML Wed Apr 10 15:30:19 2013 +0200
@@ -1746,12 +1746,12 @@
THEN ALLGOALS (rtac @{thm refl});
fun mk_eq thy eq_def =
Simplifier.rewrite_rule
- [AxClass.unoverload thy (Thm.symmetric (Simpdata.mk_eq eq_def))] inject;
+ [Axclass.unoverload thy (Thm.symmetric (Simpdata.mk_eq eq_def))] inject;
fun mk_eq_refl thy =
@{thm equal_refl}
|> Thm.instantiate
([pairself (ctyp_of thy) (TVar (("'a", 0), @{sort equal}), Logic.varifyT_global extT)], [])
- |> AxClass.unoverload thy;
+ |> Axclass.unoverload thy;
val ensure_random_record = ensure_sort_record (@{sort random}, mk_random_eq);
val ensure_exhaustive_record =
ensure_sort_record (@{sort full_exhaustive}, mk_full_exhaustive_eq);
--- a/src/Pure/Isar/class.ML Wed Apr 10 13:10:38 2013 +0200
+++ b/src/Pure/Isar/class.ML Wed Apr 10 15:30:19 2013 +0200
@@ -127,7 +127,7 @@
let
fun params class =
let
- val const_typs = (#params o AxClass.get_info thy) class;
+ val const_typs = (#params o Axclass.get_info thy) class;
val const_names = (#consts o the_class_data thy) class;
in
(map o apsnd)
@@ -190,7 +190,7 @@
([Pretty.command "class", Pretty.brk 1,
Pretty.mark_str (Name_Space.markup_extern ctxt class_space class), Pretty.str ":",
Pretty.fbrk, Pretty.block [Pretty.str "supersort: ", prt_supersort class]] @
- (case try (AxClass.get_info thy) class of
+ (case try (Axclass.get_info thy) class of
NONE => []
| SOME {params, ...} =>
[Pretty.fbrk, Pretty.big_list "parameters:" (map prt_param params)]) @
@@ -263,7 +263,7 @@
| NONE => I);
in
thy
- |> AxClass.add_classrel classrel
+ |> Axclass.add_classrel classrel
|> Class_Data.map (Graph.add_edge (sub, sup))
|> activate_defs sub (these_defs thy diff_sort)
|> add_dependency
@@ -401,7 +401,7 @@
fun gen_classrel mk_prop classrel thy =
let
fun after_qed results =
- Proof_Context.background_theory ((fold o fold) AxClass.add_classrel results);
+ Proof_Context.background_theory ((fold o fold) Axclass.add_classrel results);
in
thy
|> Proof_Context.init_global
@@ -411,9 +411,9 @@
in
val classrel =
- gen_classrel (Logic.mk_classrel oo AxClass.cert_classrel);
+ gen_classrel (Logic.mk_classrel oo Axclass.cert_classrel);
val classrel_cmd =
- gen_classrel (Logic.mk_classrel oo AxClass.read_classrel);
+ gen_classrel (Logic.mk_classrel oo Axclass.read_classrel);
end; (*local*)
@@ -472,7 +472,7 @@
let
val Instantiation {params, ...} = Instantiation.get ctxt;
- val lookup_inst_param = AxClass.lookup_inst_param
+ val lookup_inst_param = Axclass.lookup_inst_param
(Sign.consts_of (Proof_Context.theory_of ctxt)) params;
fun subst (c, ty) =
(case lookup_inst_param (c, ty) of
@@ -505,8 +505,8 @@
(* target *)
fun define_overloaded (c, U) v (b_def, rhs) =
- Local_Theory.background_theory_result (AxClass.declare_overloaded (c, U)
- ##>> AxClass.define_overloaded b_def (c, rhs))
+ Local_Theory.background_theory_result (Axclass.declare_overloaded (c, U)
+ ##>> Axclass.define_overloaded b_def (c, rhs))
##> (map_instantiation o apsnd) (filter_out (fn (_, (v', _)) => v' = v))
##> Local_Theory.map_contexts (K synchronize_inst_syntax);
@@ -541,9 +541,9 @@
val naming = Sign.naming_of thy;
val _ = if null tycos then error "At least one arity must be given" else ();
- val class_params = these_params thy (filter (can (AxClass.get_info thy)) sort);
+ val class_params = these_params thy (filter (can (Axclass.get_info thy)) sort);
fun get_param tyco (param, (_, (c, ty))) =
- if can (AxClass.param_of_inst thy) (c, tyco)
+ if can (Axclass.param_of_inst thy) (c, tyco)
then NONE else SOME ((c, tyco),
(param ^ "_" ^ Long_Name.base_name tyco, map_atyps (K (Type (tyco, map TFree vs))) ty));
val params = map_product get_param tycos class_params |> map_filter I;
@@ -559,7 +559,7 @@
val improve_constraints = AList.lookup (op =)
(map (fn (_, (class, (c, _))) => (c, [[class]])) class_params);
fun resort_check ctxt ts = resort_terms ctxt algebra consts improve_constraints ts;
- val lookup_inst_param = AxClass.lookup_inst_param consts params;
+ val lookup_inst_param = Axclass.lookup_inst_param consts params;
fun improve (c, ty) =
(case lookup_inst_param (c, ty) of
SOME (_, ty') => if Sign.typ_instance thy (ty', ty) then SOME (ty, ty') else NONE
@@ -593,7 +593,7 @@
val (tycos, vs, sort) = (#arities o the_instantiation) lthy;
val arities_proof = maps (fn tyco => Logic.mk_arities (tyco, map snd vs, sort)) tycos;
fun after_qed' results =
- Local_Theory.background_theory (fold (AxClass.add_arity o Thm.varifyT_global) results)
+ Local_Theory.background_theory (fold (Axclass.add_arity o Thm.varifyT_global) results)
#> after_qed;
in
lthy
@@ -630,7 +630,7 @@
val sorts = map snd vs;
val arities = maps (fn tyco => Logic.mk_arities (tyco, sorts, sort)) tycos;
fun after_qed results =
- Proof_Context.background_theory ((fold o fold) AxClass.add_arity results);
+ Proof_Context.background_theory ((fold o fold) Axclass.add_arity results);
in
thy
|> Proof_Context.init_global
@@ -645,7 +645,7 @@
val thy = Thm.theory_of_thm st;
val classes = Sign.all_classes thy;
val class_trivs = map (Thm.class_triv thy) classes;
- val class_intros = map_filter (try (#intro o AxClass.get_info thy)) classes;
+ val class_intros = map_filter (try (#intro o Axclass.get_info thy)) classes;
val assm_intros = all_assm_intros thy;
in
Method.intros_tac (class_trivs @ class_intros @ assm_intros) facts st
--- a/src/Pure/Isar/class_declaration.ML Wed Apr 10 13:10:38 2013 +0200
+++ b/src/Pure/Isar/class_declaration.ML Wed Apr 10 15:30:19 2013 +0200
@@ -90,7 +90,7 @@
((map_types o map_atyps) (K aT) prop), of_class_prop_concl));
val sup_of_classes = map (snd o Class.rules thy) sups;
val loc_axiom_intros = map Drule.export_without_context_open (Locale.axioms_of thy class);
- val axclass_intro = #intro (AxClass.get_info thy class);
+ val axclass_intro = #intro (Axclass.get_info thy class);
val base_sort_trivs = Thm.of_sort (Thm.ctyp_of thy aT, base_sort);
val tac =
REPEAT (SOMEGOAL
@@ -289,13 +289,13 @@
|> fst
|> Option.map (Logic.unvarify_global o Logic.strip_imp_concl o Thm.prop_of);
fun get_axiom thy =
- (case #axioms (AxClass.get_info thy class) of
+ (case #axioms (Axclass.get_info thy class) of
[] => NONE
| [thm] => SOME thm);
in
thy
|> add_consts class base_sort sups supparam_names global_syntax
- |-> (fn (param_map, params) => AxClass.define_class (bname, supsort)
+ |-> (fn (param_map, params) => Axclass.define_class (bname, supsort)
(map (fst o snd) params)
[(Thm.empty_binding, Option.map (globalize param_map) raw_pred |> the_list)]
#> snd
@@ -346,7 +346,7 @@
(case Named_Target.peek lthy of
SOME {target, is_class = true, ...} => target
| _ => error "Not in a class target");
- val (sub, sup) = AxClass.cert_classrel thy (proto_sub, proto_sup);
+ val (sub, sup) = Axclass.cert_classrel thy (proto_sub, proto_sup);
val expr = ([(sup, (("", false), Expression.Positional []))], []);
val (([props], deps, export), goal_ctxt) =
--- a/src/Pure/Isar/code.ML Wed Apr 10 13:10:38 2013 +0200
+++ b/src/Pure/Isar/code.ML Wed Apr 10 15:30:19 2013 +0200
@@ -107,7 +107,7 @@
fun string_of_const thy c =
let val ctxt = Proof_Context.init_global thy in
- case AxClass.inst_of_param thy c of
+ case Axclass.inst_of_param thy c of
SOME (c, tyco) =>
Proof_Context.extern_const ctxt c ^ " " ^ enclose "[" "]"
(Proof_Context.extern_type ctxt tyco)
@@ -140,7 +140,7 @@
fun check_unoverload thy (c, ty) =
let
- val c' = AxClass.unoverload_const thy (c, ty);
+ val c' = Axclass.unoverload_const thy (c, ty);
val ty_decl = Sign.the_const_type thy c';
in
if typscheme_equiv (ty_decl, Logic.varifyT_global ty)
@@ -375,7 +375,7 @@
fun constrset_of_consts thy consts =
let
- val _ = map (fn (c, _) => if (is_some o AxClass.class_of_param thy) c
+ val _ = map (fn (c, _) => if (is_some o Axclass.class_of_param thy) c
then error ("Is a class parameter: " ^ string_of_const thy c) else ()) consts;
val raw_constructors = map (analyze_constructor thy) consts;
val tyco = case distinct (op =) (map (fst o fst) raw_constructors)
@@ -477,7 +477,7 @@
else bad_thm "Free type variables on right hand side of equation";
val (head, args) = strip_comb lhs;
val (c, ty) = case head
- of Const (c_ty as (_, ty)) => (AxClass.unoverload_const thy c_ty, ty)
+ of Const (c_ty as (_, ty)) => (Axclass.unoverload_const thy c_ty, ty)
| _ => bad_thm "Equation not headed by constant";
fun check _ (Abs _) = bad_thm "Abstraction on left hand side of equation"
| check 0 (Var _) = ()
@@ -485,7 +485,7 @@
| check n (t1 $ t2) = (check (n+1) t1; check 0 t2)
| check n (Const (c_ty as (c, ty))) =
if allow_pats then let
- val c' = AxClass.unoverload_const thy c_ty
+ val c' = Axclass.unoverload_const thy c_ty
in if n = (length o binder_types) ty
then if allow_consts orelse is_constr thy c'
then ()
@@ -495,7 +495,7 @@
val _ = map (check 0) args;
val _ = if allow_nonlinear orelse is_linear thm then ()
else bad_thm "Duplicate variables on left hand side of equation";
- val _ = if (is_none o AxClass.class_of_param thy) c then ()
+ val _ = if (is_none o Axclass.class_of_param thy) c then ()
else bad_thm "Overloaded constant as head in equation";
val _ = if not (is_constr thy c) then ()
else bad_thm "Constructor as head in equation";
@@ -557,13 +557,13 @@
fun const_typ_eqn thy thm =
let
val (c, ty) = head_eqn thm;
- val c' = AxClass.unoverload_const thy (c, ty);
+ val c' = Axclass.unoverload_const thy (c, ty);
(*permissive wrt. to overloaded constants!*)
in (c', ty) end;
fun const_eqn thy = fst o const_typ_eqn thy;
-fun const_abs_eqn thy = AxClass.unoverload_const thy o dest_Const o fst o strip_comb o snd
+fun const_abs_eqn thy = Axclass.unoverload_const thy o dest_Const o fst o strip_comb o snd
o dest_comb o fst o Logic.dest_equals o Thm.plain_prop_of;
fun mk_proj tyco vs ty abs rep =
@@ -629,14 +629,14 @@
fun check_abstype_cert thy proto_thm =
let
- val thm = (AxClass.unoverload thy o meta_rewrite thy) proto_thm;
+ val thm = (Axclass.unoverload thy o meta_rewrite thy) proto_thm;
val (lhs, rhs) = Logic.dest_equals (Thm.plain_prop_of thm)
handle TERM _ => bad_thm "Not an equation"
| THM _ => bad_thm "Not a proper equation";
val ((abs, raw_ty), ((rep, rep_ty), param)) = (apsnd (apfst dest_Const o dest_comb)
o apfst dest_Const o dest_comb) lhs
handle TERM _ => bad_thm "Not an abstype certificate";
- val _ = pairself (fn c => if (is_some o AxClass.class_of_param thy) c
+ val _ = pairself (fn c => if (is_some o Axclass.class_of_param thy) c
then error ("Is a class parameter: " ^ string_of_const thy c) else ()) (abs, rep);
val _ = check_decl_ty thy (abs, raw_ty);
val _ = check_decl_ty thy (rep, rep_ty);
@@ -714,7 +714,7 @@
let
val raw_ty = Logic.unvarifyT_global (const_typ thy c);
val (vs, _) = typscheme thy (c, raw_ty);
- val sortargs = case AxClass.class_of_param thy c
+ val sortargs = case Axclass.class_of_param thy c
of SOME class => [[class]]
| NONE => (case get_type_of_constr_or_abstr thy c
of SOME (tyco, _) => (map snd o fst o the)
@@ -840,12 +840,12 @@
end;
fun pretty_cert thy (cert as Equations _) =
- (map_filter (Option.map (Display.pretty_thm_global thy o AxClass.overload thy) o fst o snd)
+ (map_filter (Option.map (Display.pretty_thm_global thy o Axclass.overload thy) o fst o snd)
o snd o equations_of_cert thy) cert
| pretty_cert thy (Projection (t, _)) =
[Syntax.pretty_term_global thy (Logic.varify_types_global t)]
| pretty_cert thy (Abstract (abs_thm, _)) =
- [(Display.pretty_thm_global thy o AxClass.overload thy o Thm.varifyT_global) abs_thm];
+ [(Display.pretty_thm_global thy o Axclass.overload thy o Thm.varifyT_global) abs_thm];
fun bare_thms_of_cert thy (cert as Equations _) =
(map_filter (fn (_, (some_thm, proper)) => if proper then some_thm else NONE)
@@ -881,7 +881,7 @@
(map o apfst) (Thm.transfer thy)
#> perhaps (perhaps_loop (perhaps_apply functrans))
#> (map o apfst) (rewrite_eqn thy eqn_conv ss)
- #> (map o apfst) (AxClass.unoverload thy)
+ #> (map o apfst) (Axclass.unoverload thy)
#> cert_of_eqns thy c;
fun get_cert thy { functrans, ss } c =
@@ -895,7 +895,7 @@
| Abstr (abs_thm, tyco) => abs_thm
|> Thm.transfer thy
|> rewrite_eqn thy Conv.arg_conv ss
- |> AxClass.unoverload thy
+ |> Axclass.unoverload thy
|> cert_of_abs thy tyco c;
@@ -1172,7 +1172,7 @@
#> (map_cases o apfst) drop_outdated_cases)
end;
-fun unoverload_const_typ thy (c, ty) = (AxClass.unoverload_const thy (c, ty), ty);
+fun unoverload_const_typ thy (c, ty) = (Axclass.unoverload_const thy (c, ty), ty);
structure Datatype_Interpretation =
Interpretation(type T = string * serial val eq = eq_snd (op =) : T * T -> bool);
--- a/src/Pure/Isar/isar_syn.ML Wed Apr 10 13:10:38 2013 +0200
+++ b/src/Pure/Isar/isar_syn.ML Wed Apr 10 15:30:19 2013 +0200
@@ -79,13 +79,13 @@
Outer_Syntax.command @{command_spec "classes"} "declare type classes"
(Scan.repeat1 (Parse.binding -- Scan.optional ((@{keyword "\<subseteq>"} || @{keyword "<"}) |--
Parse.!!! (Parse.list1 Parse.class)) [])
- >> (Toplevel.theory o fold AxClass.axiomatize_class_cmd));
+ >> (Toplevel.theory o fold Axclass.axiomatize_class_cmd));
val _ =
Outer_Syntax.command @{command_spec "classrel"} "state inclusion of type classes (axiomatic!)"
(Parse.and_list1 (Parse.class -- ((@{keyword "\<subseteq>"} || @{keyword "<"})
|-- Parse.!!! Parse.class))
- >> (Toplevel.theory o AxClass.axiomatize_classrel_cmd));
+ >> (Toplevel.theory o Axclass.axiomatize_classrel_cmd));
val _ =
Outer_Syntax.local_theory @{command_spec "default_sort"}
@@ -113,7 +113,7 @@
val _ =
Outer_Syntax.command @{command_spec "arities"} "state type arities (axiomatic!)"
- (Scan.repeat1 Parse.arity >> (Toplevel.theory o fold AxClass.axiomatize_arity_cmd));
+ (Scan.repeat1 Parse.arity >> (Toplevel.theory o fold Axclass.axiomatize_arity_cmd));
(* consts and syntax *)
--- a/src/Pure/Isar/typedecl.ML Wed Apr 10 13:10:38 2013 +0200
+++ b/src/Pure/Isar/typedecl.ML Wed Apr 10 15:30:19 2013 +0200
@@ -29,7 +29,7 @@
fun object_logic_arity name thy =
(case Object_Logic.get_base_sort thy of
NONE => thy
- | SOME S => AxClass.axiomatize_arity (name, replicate (Sign.arity_number thy name) S, S) thy);
+ | SOME S => Axclass.axiomatize_arity (name, replicate (Sign.arity_number thy name) S, S) thy);
fun basic_decl decl (b, n, mx) lthy =
let val name = Local_Theory.full_name lthy b in
--- a/src/Pure/axclass.ML Wed Apr 10 13:10:38 2013 +0200
+++ b/src/Pure/axclass.ML Wed Apr 10 15:30:19 2013 +0200
@@ -5,7 +5,7 @@
parameters. Proven class relations and type arities.
*)
-signature AX_CLASS =
+signature AXCLASS =
sig
type info = {def: thm, intro: thm, axioms: thm list, params: (string * typ) list}
val get_info: theory -> class -> info
@@ -38,7 +38,7 @@
val axiomatize_arity_cmd: xstring * string list * string -> theory -> theory
end;
-structure AxClass: AX_CLASS =
+structure Axclass: AXCLASS =
struct
(** theory data **)
--- a/src/Tools/Code/code_preproc.ML Wed Apr 10 13:10:38 2013 +0200
+++ b/src/Tools/Code/code_preproc.ML Wed Apr 10 15:30:19 2013 +0200
@@ -143,7 +143,7 @@
val pre = (Simplifier.global_context thy o #pre o the_thmproc) thy;
in
Simplifier.rewrite pre
- #> trans_conv_rule (AxClass.unoverload_conv thy)
+ #> trans_conv_rule (Axclass.unoverload_conv thy)
end;
fun preprocess_term thy = term_of_conv_resubst thy (preprocess_conv thy);
@@ -152,7 +152,7 @@
let
val post = (Simplifier.global_context thy o #post o the_thmproc) thy;
in
- AxClass.overload_conv thy
+ Axclass.overload_conv thy
#> trans_conv_rule (Simplifier.rewrite post)
end;
@@ -213,14 +213,14 @@
(* auxiliary *)
-fun is_proper_class thy = can (AxClass.get_info thy);
+fun is_proper_class thy = can (Axclass.get_info thy);
fun complete_proper_sort thy =
Sign.complete_sort thy #> filter (is_proper_class thy);
fun inst_params thy tyco =
- map (fn (c, _) => AxClass.param_of_inst thy (c, tyco))
- o maps (#params o AxClass.get_info thy);
+ map (fn (c, _) => Axclass.param_of_inst thy (c, tyco))
+ o maps (#params o Axclass.get_info thy);
(* data structures *)
--- a/src/Tools/Code/code_target.ML Wed Apr 10 13:10:38 2013 +0200
+++ b/src/Tools/Code/code_target.ML Wed Apr 10 15:30:19 2013 +0200
@@ -544,7 +544,7 @@
fun cert_class thy class =
let
- val _ = AxClass.get_info thy class;
+ val _ = Axclass.get_info thy class;
in class end;
fun read_class thy = cert_class thy o Sign.intern_class thy;
--- a/src/Tools/Code/code_thingol.ML Wed Apr 10 13:10:38 2013 +0200
+++ b/src/Tools/Code/code_thingol.ML Wed Apr 10 15:30:19 2013 +0200
@@ -269,10 +269,10 @@
local
fun thyname_of_type thy = #theory_name o Name_Space.the_entry (Sign.type_space thy);
fun thyname_of_class thy = #theory_name o Name_Space.the_entry (Sign.class_space thy);
- fun thyname_of_instance thy inst = case AxClass.thynames_of_arity thy inst
+ fun thyname_of_instance thy inst = case Axclass.thynames_of_arity thy inst
of [] => error ("No such instance: " ^ quote (snd inst ^ " :: " ^ fst inst))
| thyname :: _ => thyname;
- fun thyname_of_const thy c = case AxClass.class_of_param thy c
+ fun thyname_of_const thy c = case Axclass.class_of_param thy c
of SOME class => thyname_of_class thy class
| NONE => (case Code.get_type_of_constr_or_abstr thy c
of SOME (tyco, _) => thyname_of_type thy tyco
@@ -662,14 +662,14 @@
end;
val stmt_const = case Code.get_type_of_constr_or_abstr thy c
of SOME (tyco, _) => stmt_datatypecons tyco
- | NONE => (case AxClass.class_of_param thy c
+ | NONE => (case Axclass.class_of_param thy c
of SOME class => stmt_classparam class
| NONE => stmt_fun (Code_Preproc.cert eqngr c))
in ensure_stmt lookup_const (declare_const thy) stmt_const c end
and ensure_class thy (algbr as (_, algebra)) eqngr permissive class =
let
val super_classes = (Sorts.minimize_sort algebra o Sorts.super_classes algebra) class;
- val cs = #params (AxClass.get_info thy class);
+ val cs = #params (Axclass.get_info thy class);
val stmt_class =
fold_map (fn super_class => ensure_class thy algbr eqngr permissive super_class
##>> ensure_classrel thy algbr eqngr permissive (class, super_class)) super_classes
@@ -687,7 +687,7 @@
and ensure_inst thy (algbr as (_, algebra)) eqngr permissive (class, tyco) =
let
val super_classes = (Sorts.minimize_sort algebra o Sorts.super_classes algebra) class;
- val these_class_params = these o try (#params o AxClass.get_info thy);
+ val these_class_params = these o try (#params o Axclass.get_info thy);
val class_params = these_class_params class;
val superclass_params = maps these_class_params
((Sorts.complete_sort algebra o Sorts.super_classes algebra) class);
@@ -706,7 +706,7 @@
fun translate_classparam_instance (c, ty) =
let
val raw_const = Const (c, map_type_tfree (K arity_typ') ty);
- val thm = AxClass.unoverload_conv thy (Thm.cterm_of thy raw_const);
+ val thm = Axclass.unoverload_conv thy (Thm.cterm_of thy raw_const);
val const = (apsnd Logic.unvarifyT_global o dest_Const o snd
o Logic.dest_equals o Thm.prop_of) thm;
in
--- a/src/Tools/nbe.ML Wed Apr 10 13:10:38 2013 +0200
+++ b/src/Tools/nbe.ML Wed Apr 10 15:30:19 2013 +0200
@@ -56,7 +56,7 @@
of SOME T_class => T_class
| _ => error ("Bad certificate: " ^ Display.string_of_thm_global thy thm);
val tvar = case try Term.dest_TVar T
- of SOME (tvar as (_, sort)) => if null (filter (can (AxClass.get_info thy)) sort)
+ of SOME (tvar as (_, sort)) => if null (filter (can (Axclass.get_info thy)) sort)
then tvar
else error ("Bad sort: " ^ Display.string_of_thm_global thy thm)
| _ => error ("Bad type: " ^ Display.string_of_thm_global thy thm);
@@ -65,11 +65,11 @@
val lhs_rhs = case try Logic.dest_equals eqn
of SOME lhs_rhs => lhs_rhs
| _ => error ("Not an equation: " ^ Syntax.string_of_term_global thy eqn);
- val c_c' = case try (pairself (AxClass.unoverload_const thy o dest_Const)) lhs_rhs
+ val c_c' = case try (pairself (Axclass.unoverload_const thy o dest_Const)) lhs_rhs
of SOME c_c' => c_c'
| _ => error ("Not an equation with two constants: "
^ Syntax.string_of_term_global thy eqn);
- val _ = if the_list (AxClass.class_of_param thy (snd c_c')) = [class] then ()
+ val _ = if the_list (Axclass.class_of_param thy (snd c_c')) = [class] then ()
else error ("Inconsistent class: " ^ Display.string_of_thm_global thy thm);
in Triv_Class_Data.map (AList.update (op =) (class, thm)) thy end;