--- a/src/Doc/more_antiquote.ML Mon May 09 17:23:19 2016 +0100
+++ b/src/Doc/more_antiquote.ML Mon May 09 17:32:26 2016 +0100
@@ -50,7 +50,7 @@
|> snd
|> these
|> 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 ctxt);
in Thy_Output.output ctxt (Thy_Output.maybe_pretty_source pretty_thm ctxt source thms) end;
in
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML Mon May 09 17:23:19 2016 +0100
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML Mon May 09 17:32:26 2016 +0100
@@ -23,11 +23,11 @@
val reflN = "refl"
val simpsN = "simps"
-fun mk_case_certificate thy raw_thms =
+fun mk_case_certificate ctxt raw_thms =
let
val thms as thm1 :: _ = raw_thms
|> Conjunction.intr_balanced
- |> Thm.unvarify_global thy
+ |> Thm.unvarify_global (Proof_Context.theory_of ctxt)
|> Conjunction.elim_balanced (length raw_thms)
|> map Simpdata.mk_meta_eq
|> map Drule.zero_var_indexes;
@@ -36,14 +36,14 @@
|> Thm.prop_of |> Logic.dest_equals |> fst |> Term.strip_comb
||> fst o split_last |> list_comb;
val lhs = Free (singleton (Name.variant_list params) "case", Term.fastype_of rhs);
- val assum = Thm.global_cterm_of thy (Logic.mk_equals (lhs, rhs));
+ val assum = Thm.cterm_of ctxt (Logic.mk_equals (lhs, rhs));
in
thms
|> Conjunction.intr_balanced
- |> rewrite_rule (Proof_Context.init_global thy) [Thm.symmetric (Thm.assume assum)]
+ |> rewrite_rule ctxt [Thm.symmetric (Thm.assume assum)]
|> Thm.implies_intr assum
|> Thm.generalize ([], params) 0
- |> Axclass.unoverload thy
+ |> Axclass.unoverload ctxt
|> Thm.varifyT_global
end;
@@ -128,7 +128,7 @@
thy
|> Code.add_datatype ctrs
|> fold_rev Code.add_default_eqn case_thms
- |> Code.add_case (mk_case_certificate thy case_thms)
+ |> Code.add_case (mk_case_certificate (Proof_Context.init_global thy) case_thms)
|> not (Sorts.has_instance (Sign.classes_of thy) fcT_name [HOLogic.class_equal])
? add_equality fcT fcT_name As ctrs inject_thms distinct_thms
else
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Mon May 09 17:23:19 2016 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Mon May 09 17:32:26 2016 +0100
@@ -112,7 +112,9 @@
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 (Proof_Context.init_global 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/record.ML Mon May 09 17:23:19 2016 +0100
+++ b/src/HOL/Tools/record.ML Mon May 09 17:32:26 2016 +0100
@@ -1764,14 +1764,14 @@
Class.intro_classes_tac ctxt []
THEN rewrite_goals_tac ctxt [Simpdata.mk_eq eq_def]
THEN ALLGOALS (resolve_tac ctxt @{thms refl});
- fun mk_eq thy eq_def =
- rewrite_rule (Proof_Context.init_global thy)
- [Axclass.unoverload thy (Thm.symmetric (Simpdata.mk_eq eq_def))] inject;
- fun mk_eq_refl thy =
+ fun mk_eq ctxt eq_def =
+ rewrite_rule ctxt
+ [Axclass.unoverload ctxt (Thm.symmetric (Simpdata.mk_eq eq_def))] inject;
+ fun mk_eq_refl ctxt =
@{thm equal_refl}
|> Thm.instantiate
- ([((("'a", 0), @{sort equal}), Thm.global_ctyp_of thy (Logic.varifyT_global extT))], [])
- |> Axclass.unoverload thy;
+ ([((("'a", 0), @{sort equal}), Thm.ctyp_of ctxt (Logic.varifyT_global extT))], [])
+ |> Axclass.unoverload ctxt;
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);
@@ -1785,8 +1785,10 @@
|-> (fn (_, (_, eq_def)) =>
Class.prove_instantiation_exit_result Morphism.thm tac eq_def)
|-> (fn eq_def => fn thy =>
- thy |> Code.del_eqn eq_def |> Code.add_default_eqn (mk_eq thy eq_def))
- |> (fn thy => Code.add_nbe_default_eqn (mk_eq_refl thy) thy)
+ thy
+ |> Code.del_eqn eq_def
+ |> Code.add_default_eqn (mk_eq (Proof_Context.init_global thy) eq_def))
+ |> (fn thy => Code.add_nbe_default_eqn (mk_eq_refl (Proof_Context.init_global thy)) thy)
|> ensure_random_record ext_tyco vs (fst ext) (binder_types (snd ext))
|> ensure_exhaustive_record ext_tyco vs (fst ext) (binder_types (snd ext))
end
--- a/src/Pure/Isar/code.ML Mon May 09 17:23:19 2016 +0100
+++ b/src/Pure/Isar/code.ML Mon May 09 17:32:26 2016 +0100
@@ -655,7 +655,7 @@
fun check_abstype_cert thy proto_thm =
let
- val thm = (Axclass.unoverload thy o meta_rewrite thy) proto_thm;
+ val thm = (Axclass.unoverload (Proof_Context.init_global 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";
@@ -888,12 +888,15 @@
fun pretty_cert thy (cert as Nothing _) =
[Pretty.str "(not implemented)"]
| pretty_cert thy (cert as Equations _) =
- (map_filter (Option.map (Thm.pretty_thm_global thy o Axclass.overload thy) o fst o snd)
+ (map_filter
+ (Option.map (Thm.pretty_thm_global thy o
+ Axclass.overload (Proof_Context.init_global thy)) o fst o snd)
o these 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, _)) =
- [(Thm.pretty_thm_global thy o Axclass.overload thy o Thm.varifyT_global) abs_thm];
+ [(Thm.pretty_thm_global thy o
+ Axclass.overload (Proof_Context.init_global thy) o Thm.varifyT_global) abs_thm];
end;
@@ -916,13 +919,9 @@
singleton (Variable.trade (K (map (Conv.fconv_rule (conv (Simplifier.rewrite ctxt))))) ctxt)
fun preprocess conv ctxt =
- let
- val thy = Proof_Context.theory_of ctxt;
- in
- Thm.transfer thy
- #> rewrite_eqn conv ctxt
- #> Axclass.unoverload thy
- end;
+ Thm.transfer (Proof_Context.theory_of ctxt)
+ #> rewrite_eqn conv ctxt
+ #> Axclass.unoverload ctxt;
fun cert_of_eqns_preprocess ctxt functrans c =
let
--- a/src/Pure/axclass.ML Mon May 09 17:23:19 2016 +0100
+++ b/src/Pure/axclass.ML Mon May 09 17:32:26 2016 +0100
@@ -14,10 +14,10 @@
val thynames_of_arity: theory -> string * class -> string list
val param_of_inst: theory -> string * string -> string
val inst_of_param: theory -> string -> (string * string) option
- val unoverload: theory -> thm -> thm
- val overload: theory -> thm -> thm
- val unoverload_conv: theory -> conv
- val overload_conv: theory -> conv
+ val unoverload: Proof.context -> thm -> thm
+ val overload: Proof.context -> thm -> thm
+ val unoverload_conv: Proof.context -> conv
+ val overload_conv: Proof.context -> conv
val lookup_inst_param: Consts.T -> ((string * string) * 'a) list -> string * typ -> 'a option
val unoverload_const: theory -> string * typ -> string
val cert_classrel: theory -> class * class -> class * class
@@ -284,22 +284,17 @@
val inst_of_param = Symtab.lookup o #2 o inst_params_of;
val param_of_inst = #1 oo get_inst_param;
-fun inst_thms thy =
- Symtab.fold (Symtab.fold (cons o #2 o #2) o #2) (#1 (inst_params_of thy)) [];
+fun inst_thms ctxt =
+ Symtab.fold
+ (Symtab.fold (cons o #2 o #2) o #2) (#1 (inst_params_of (Proof_Context.theory_of ctxt))) [];
fun get_inst_tyco consts = try (#1 o dest_Type o the_single o Consts.typargs consts);
-fun unoverload thy =
- rewrite_rule (Proof_Context.init_global thy) (inst_thms thy);
-
-fun overload thy =
- rewrite_rule (Proof_Context.init_global thy) (map Thm.symmetric (inst_thms thy));
+fun unoverload ctxt = rewrite_rule ctxt (inst_thms ctxt);
+fun overload ctxt = rewrite_rule ctxt (map Thm.symmetric (inst_thms ctxt));
-fun unoverload_conv thy =
- Raw_Simplifier.rewrite (Proof_Context.init_global thy) true (inst_thms thy);
-
-fun overload_conv thy =
- Raw_Simplifier.rewrite (Proof_Context.init_global thy) true (map Thm.symmetric (inst_thms thy));
+fun unoverload_conv ctxt = Raw_Simplifier.rewrite ctxt true (inst_thms ctxt);
+fun overload_conv ctxt = Raw_Simplifier.rewrite ctxt true (map Thm.symmetric (inst_thms ctxt));
fun lookup_inst_param consts params (c, T) =
(case get_inst_tyco consts (c, T) of
--- a/src/Tools/Code/code_preproc.ML Mon May 09 17:23:19 2016 +0100
+++ b/src/Tools/Code/code_preproc.ML Mon May 09 17:32:26 2016 +0100
@@ -205,9 +205,9 @@
val post = (#post o the_thmproc) thy;
fun pre_conv ctxt' =
Simplifier.rewrite (put_simpset pre ctxt')
- #> trans_conv_rule (Axclass.unoverload_conv (Proof_Context.theory_of ctxt'))
+ #> trans_conv_rule (Axclass.unoverload_conv ctxt')
fun post_conv ctxt' =
- Axclass.overload_conv (Proof_Context.theory_of ctxt')
+ Axclass.overload_conv ctxt'
#> trans_conv_rule (Simplifier.rewrite (put_simpset post ctxt'))
in fn ctxt' => pre_conv ctxt' #> pair (post_conv ctxt') end;
--- a/src/Tools/Code/code_thingol.ML Mon May 09 17:23:19 2016 +0100
+++ b/src/Tools/Code/code_thingol.ML Mon May 09 17:32:26 2016 +0100
@@ -574,7 +574,7 @@
let
val raw_const = Const (c, map_type_tfree (K arity_typ') ty);
val dom_length = length (fst (strip_type ty))
- val thm = Axclass.unoverload_conv thy (Thm.cterm_of ctxt raw_const);
+ val thm = Axclass.unoverload_conv ctxt (Thm.cterm_of ctxt raw_const);
val const = (apsnd Logic.unvarifyT_global o dest_Const o snd
o Logic.dest_equals o Thm.prop_of) thm;
in