# HG changeset patch
# User wenzelm
# Date 1462807352 -7200
# Node ID c607302955994713943f4969d17b9d72fe6c27e4
# Parent  eb5d493a9e03ed4e048f3bc3c6b667046335ba12# Parent  413184c7a2a270046279ca6dd9275a7bee4b763c
merged

diff -r eb5d493a9e03 -r c60730295599 src/Doc/more_antiquote.ML
--- a/src/Doc/more_antiquote.ML	Mon May 09 16:02:23 2016 +0100
+++ b/src/Doc/more_antiquote.ML	Mon May 09 17:22:32 2016 +0200
@@ -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
diff -r eb5d493a9e03 -r c60730295599 src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML	Mon May 09 16:02:23 2016 +0100
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML	Mon May 09 17:22:32 2016 +0200
@@ -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
diff -r eb5d493a9e03 -r c60730295599 src/HOL/Tools/Predicate_Compile/predicate_compile.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Mon May 09 16:02:23 2016 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Mon May 09 17:22:32 2016 +0200
@@ -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; ()))
diff -r eb5d493a9e03 -r c60730295599 src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Mon May 09 16:02:23 2016 +0100
+++ b/src/HOL/Tools/record.ML	Mon May 09 17:22:32 2016 +0200
@@ -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
diff -r eb5d493a9e03 -r c60730295599 src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Mon May 09 16:02:23 2016 +0100
+++ b/src/Pure/Isar/code.ML	Mon May 09 17:22:32 2016 +0200
@@ -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
diff -r eb5d493a9e03 -r c60730295599 src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Mon May 09 16:02:23 2016 +0100
+++ b/src/Pure/axclass.ML	Mon May 09 17:22:32 2016 +0200
@@ -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
diff -r eb5d493a9e03 -r c60730295599 src/Tools/Code/code_preproc.ML
--- a/src/Tools/Code/code_preproc.ML	Mon May 09 16:02:23 2016 +0100
+++ b/src/Tools/Code/code_preproc.ML	Mon May 09 17:22:32 2016 +0200
@@ -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;
 
diff -r eb5d493a9e03 -r c60730295599 src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Mon May 09 16:02:23 2016 +0100
+++ b/src/Tools/Code/code_thingol.ML	Mon May 09 17:22:32 2016 +0200
@@ -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