# HG changeset patch
# User wenzelm
# Date 1425681539 -3600
# Node ID c9aa1c90796f5079e851ec4c1ae13fba40669876
# Parent  0d77c51b5040155c4420b4bba37874c0df211f85
clarified context;

diff -r 0d77c51b5040 -r c9aa1c90796f src/HOL/Tools/Lifting/lifting_def.ML
--- a/src/HOL/Tools/Lifting/lifting_def.ML	Fri Mar 06 23:33:25 2015 +0100
+++ b/src/HOL/Tools/Lifting/lifting_def.ML	Fri Mar 06 23:38:59 2015 +0100
@@ -56,8 +56,7 @@
 
 fun try_prove_reflexivity ctxt prop =
   let
-    val thy = Proof_Context.theory_of ctxt
-    val cprop = Thm.global_cterm_of thy prop
+    val cprop = Thm.cterm_of ctxt prop
     val rule = @{thm ge_eq_refl}
     val concl_pat = Drule.strip_imp_concl (Thm.cprop_of rule)
     val insts = Thm.first_order_match (concl_pat, cprop)
@@ -85,7 +84,6 @@
       let
         val tm = (strip_args 2 o HOLogic.dest_Trueprop o Thm.concl_of) thm;
         val param_rel = (snd o dest_comb o fst o dest_comb) tm;
-        val thy = Proof_Context.theory_of ctxt;
         val free_vars = Term.add_vars param_rel [];
         
         fun make_subst (var as (_, typ)) subst = 
@@ -99,7 +97,7 @@
           end;
         
         val subst = fold make_subst free_vars [];
-        val csubst = map (apply2 (Thm.global_cterm_of thy)) subst;
+        val csubst = map (apply2 (Thm.cterm_of ctxt)) subst;
         val inst_thm = Drule.cterm_instantiate csubst thm;
       in
         Conv.fconv_rule 
@@ -108,37 +106,37 @@
             (Raw_Simplifier.rewrite ctxt false (Transfer.get_sym_relator_eq ctxt))) inst_thm
       end
 
-    fun inst_relcomppI thy ant1 ant2 =
+    fun inst_relcomppI ctxt ant1 ant2 =
       let
         val t1 = (HOLogic.dest_Trueprop o Thm.concl_of) ant1
         val t2 = (HOLogic.dest_Trueprop o Thm.prop_of) ant2
-        val fun1 = Thm.global_cterm_of thy (strip_args 2 t1)
-        val args1 = map (Thm.global_cterm_of thy) (get_args 2 t1)
-        val fun2 = Thm.global_cterm_of thy (strip_args 2 t2)
-        val args2 = map (Thm.global_cterm_of thy) (get_args 1 t2)
+        val fun1 = Thm.cterm_of ctxt (strip_args 2 t1)
+        val args1 = map (Thm.cterm_of ctxt) (get_args 2 t1)
+        val fun2 = Thm.cterm_of ctxt (strip_args 2 t2)
+        val args2 = map (Thm.cterm_of ctxt) (get_args 1 t2)
         val relcomppI = Drule.incr_indexes2 ant1 ant2 @{thm relcomppI}
         val vars = (rev (Term.add_vars (Thm.prop_of relcomppI) []))
-        val subst = map (apfst (Thm.global_cterm_of thy o Var)) (vars ~~ ([fun1] @ args1 @ [fun2] @ args2))
+        val subst = map (apfst (Thm.cterm_of ctxt o Var)) (vars ~~ ([fun1] @ args1 @ [fun2] @ args2))
       in
         Drule.cterm_instantiate subst relcomppI
       end
 
     fun zip_transfer_rules ctxt thm =
       let
-        val thy = Proof_Context.theory_of ctxt
         fun mk_POS ty = Const (@{const_name POS}, ty --> ty --> HOLogic.boolT)
         val rel = (Thm.dest_fun2 o Thm.dest_arg o Thm.cprop_of) thm
         val typ = Thm.typ_of_cterm rel
-        val POS_const = Thm.global_cterm_of thy (mk_POS typ)
-        val var = Thm.global_cterm_of thy (Var (("X", Thm.maxidx_of_cterm rel + 1), typ))
+        val POS_const = Thm.cterm_of ctxt (mk_POS typ)
+        val var = Thm.cterm_of ctxt (Var (("X", Thm.maxidx_of_cterm rel + 1), typ))
         val goal =
-          Thm.apply (Thm.global_cterm_of thy HOLogic.Trueprop) (Thm.apply (Thm.apply POS_const rel) var)
+          Thm.apply (Thm.cterm_of ctxt HOLogic.Trueprop) (Thm.apply (Thm.apply POS_const rel) var)
       in
         [Lifting_Term.merge_transfer_relations ctxt goal, thm] MRSL @{thm POS_apply}
       end
      
-    val thm = (inst_relcomppI (Proof_Context.theory_of ctxt) parametric_transfer_rule transfer_rule) 
-                OF [parametric_transfer_rule, transfer_rule]
+    val thm =
+      inst_relcomppI ctxt parametric_transfer_rule transfer_rule
+        OF [parametric_transfer_rule, transfer_rule]
     val preprocessed_thm = preprocess ctxt thm
     val orig_ctxt = ctxt
     val (fixed_thm, ctxt) = yield_singleton (apfst snd oo Variable.import true) preprocessed_thm ctxt
@@ -215,8 +213,7 @@
       | dest_abs tm = raise TERM("get_abs_var",[tm])
     val (var_name, T) = dest_abs (Thm.term_of rhs)
     val (new_var_names, ctxt') = Variable.variant_fixes [var_name] ctxt
-    val thy = Proof_Context.theory_of ctxt'
-    val refl_thm = Thm.reflexive (Thm.global_cterm_of thy (Free (hd new_var_names, T)))
+    val refl_thm = Thm.reflexive (Thm.cterm_of ctxt' (Free (hd new_var_names, T)))
   in
     Thm.combination def refl_thm |>
     singleton (Proof_Context.export ctxt' ctxt)
@@ -301,7 +298,7 @@
           SOME mono_eq_thm =>
             let
               val rep_abs_eq = mono_eq_thm RS rep_abs_thm
-              val rep = (Thm.global_cterm_of thy o quot_thm_rep) quot_thm
+              val rep = Thm.cterm_of ctxt (quot_thm_rep quot_thm)
               val rep_refl = Thm.reflexive rep RS @{thm meta_eq_to_obj_eq}
               val repped_eq = [rep_refl, unabs_def RS @{thm meta_eq_to_obj_eq}] MRSL @{thm cong}
               val code_cert = [repped_eq, rep_abs_eq] MRSL trans
@@ -378,9 +375,9 @@
   end
 
 local
-  fun encode_code_eq thy abs_eq opt_rep_eq (rty, qty) = 
+  fun encode_code_eq ctxt abs_eq opt_rep_eq (rty, qty) = 
     let
-      fun mk_type typ = typ |> Logic.mk_type |> Thm.global_cterm_of thy |> Drule.mk_term
+      fun mk_type typ = typ |> Logic.mk_type |> Thm.cterm_of ctxt |> Drule.mk_term
     in
       Conjunction.intr_balanced [abs_eq, (the_default TrueI opt_rep_eq), mk_type rty, mk_type qty]
     end
@@ -429,8 +426,7 @@
 
 fun register_code_eq abs_eq_thm opt_rep_eq_thm (rty, qty) lthy =
   let
-    val thy = Proof_Context.theory_of lthy
-    val encoded_code_eq = encode_code_eq thy abs_eq_thm opt_rep_eq_thm (rty, qty)
+    val encoded_code_eq = encode_code_eq lthy abs_eq_thm opt_rep_eq_thm (rty, qty)
   in
     if no_no_code lthy (rty, qty) then 
       (snd oo Local_Theory.note) ((Binding.empty, [register_code_eq_attrib]), [encoded_code_eq]) lthy
diff -r 0d77c51b5040 -r c9aa1c90796f src/HOL/Tools/Lifting/lifting_setup.ML
--- a/src/HOL/Tools/Lifting/lifting_setup.ML	Fri Mar 06 23:33:25 2015 +0100
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Fri Mar 06 23:38:59 2015 +0100
@@ -106,10 +106,9 @@
         let 
           val typ = (snd o relation_types o snd o dest_Var) var
           val sort = Type.sort_of_atyp typ
-          val (fresh_var, ctxt) = yield_singleton Variable.invent_types sort ctxt
-          val thy = Proof_Context.theory_of ctxt
+          val (fresh_var, ctxt') = yield_singleton Variable.invent_types sort ctxt
         in
-          ((Thm.global_cterm_of thy var, Thm.global_cterm_of thy (HOLogic.eq_const (TFree fresh_var))), ctxt)
+          (apply2 (Thm.cterm_of ctxt') (var, HOLogic.eq_const (TFree fresh_var)), ctxt')
         end
       
       val orig_lthy = lthy
@@ -287,12 +286,10 @@
 in
   fun reduce_goal not_fix goal tac ctxt =
     let
-      val thy = Proof_Context.theory_of ctxt
-      val orig_ctxt = ctxt
-      val (fixed_goal, ctxt) = yield_singleton (import_terms_exclude not_fix) goal ctxt
-      val init_goal = Goal.init (Thm.global_cterm_of thy fixed_goal)
+      val (fixed_goal, ctxt') = yield_singleton (import_terms_exclude not_fix) goal ctxt
+      val init_goal = Goal.init (Thm.cterm_of ctxt' fixed_goal)
     in
-      (singleton (Variable.export ctxt orig_ctxt) o Goal.conclude) (the (SINGLE tac init_goal))
+      (singleton (Variable.export ctxt' ctxt) o Goal.conclude) (the (SINGLE tac init_goal))
     end
 end
 
@@ -304,16 +301,14 @@
     let
       fun generate_transfer_rule pcr_def constraint goal ctxt =
         let
-          val thy = Proof_Context.theory_of ctxt
-          val orig_ctxt = ctxt
-          val (fixed_goal, ctxt) = yield_singleton (Variable.import_terms true) goal ctxt
-          val init_goal = Goal.init (Thm.global_cterm_of thy fixed_goal)
-          val rules = Transfer.get_transfer_raw ctxt
+          val (fixed_goal, ctxt') = yield_singleton (Variable.import_terms true) goal ctxt
+          val init_goal = Goal.init (Thm.cterm_of ctxt' fixed_goal)
+          val rules = Transfer.get_transfer_raw ctxt'
           val rules = constraint :: OO_rules @ rules
           val tac =
-            K (Local_Defs.unfold_tac ctxt [pcr_def]) THEN' REPEAT_ALL_NEW (resolve_tac ctxt rules)
+            K (Local_Defs.unfold_tac ctxt' [pcr_def]) THEN' REPEAT_ALL_NEW (resolve_tac ctxt' rules)
         in
-          (singleton (Variable.export ctxt orig_ctxt) o Goal.conclude) (the (SINGLE (tac 1) init_goal))
+          (singleton (Variable.export ctxt' ctxt) o Goal.conclude) (the (SINGLE (tac 1) init_goal))
         end
       
       fun make_goal pcr_def constr =
@@ -371,18 +366,16 @@
 in
   fun generate_parametric_id lthy rty id_transfer_rule =
     let
-      val orig_lthy = lthy
       (* it doesn't raise an exception because it would have already raised it in define_pcrel *)
-      val (quot_thm, _, lthy) = Lifting_Term.prove_param_quot_thm lthy rty
-      val parametrized_relator = singleton (Variable.export_terms lthy orig_lthy) (quot_thm_crel quot_thm)
-      val lthy = orig_lthy
+      val (quot_thm, _, ctxt') = Lifting_Term.prove_param_quot_thm lthy rty
+      val parametrized_relator =
+        singleton (Variable.export_terms ctxt' lthy) (quot_thm_crel quot_thm)
       val id_transfer = 
          @{thm id_transfer}
         |> Thm.incr_indexes (Term.maxidx_of_term parametrized_relator + 1)
         |> Conv.fconv_rule(HOLogic.Trueprop_conv (Conv.arg_conv id_unfold then_conv Conv.arg1_conv id_unfold))
       val var = Var (hd (Term.add_vars (Thm.prop_of id_transfer) []))
-      val thy = Proof_Context.theory_of lthy
-      val inst = [(Thm.global_cterm_of thy var, Thm.global_cterm_of thy parametrized_relator)]
+      val inst = [(Thm.cterm_of lthy var, Thm.cterm_of lthy parametrized_relator)]
       val id_par_thm = Drule.cterm_instantiate inst id_transfer
     in
       Lifting_Def.generate_parametric_transfer_rule lthy id_transfer_rule id_par_thm
diff -r 0d77c51b5040 -r c9aa1c90796f src/HOL/Tools/Lifting/lifting_term.ML
--- a/src/HOL/Tools/Lifting/lifting_term.ML	Fri Mar 06 23:33:25 2015 +0100
+++ b/src/HOL/Tools/Lifting/lifting_term.ML	Fri Mar 06 23:38:59 2015 +0100
@@ -273,13 +273,13 @@
   end
   handle QUOT_THM_INTERNAL pretty_msg => raise QUOT_THM (rty, qty, pretty_msg)
 
-fun force_qty_type thy qty quot_thm =
+fun force_qty_type ctxt qty quot_thm =
   let
+    val thy = Proof_Context.theory_of ctxt
     val (_, qty_schematic) = quot_thm_rty_qty quot_thm
     val match_env = Sign.typ_match thy (qty_schematic, qty) Vartab.empty
-    fun prep_ty thy (x, (S, ty)) =
-      (Thm.global_ctyp_of thy (TVar (x, S)), Thm.global_ctyp_of thy ty)
-    val ty_inst = Vartab.fold (cons o (prep_ty thy)) match_env []
+    fun prep_ty (x, (S, ty)) = apply2 (Thm.ctyp_of ctxt) (TVar (x, S), ty)
+    val ty_inst = Vartab.fold (cons o prep_ty) match_env []
   in
     Thm.instantiate (ty_inst, []) quot_thm
   end
@@ -304,9 +304,8 @@
 
 fun prove_quot_thm ctxt (rty, qty) =
   let
-    val thy = Proof_Context.theory_of ctxt
     val schematic_quot_thm = prove_schematic_quot_thm ctxt (rty, qty)
-    val quot_thm = force_qty_type thy qty schematic_quot_thm
+    val quot_thm = force_qty_type ctxt qty schematic_quot_thm
     val _ = check_rty_type ctxt rty quot_thm
   in
     quot_thm
@@ -371,9 +370,8 @@
       if null tys 
       then 
         let 
-          val thy = Proof_Context.theory_of ctxt
           val instantiated_id_quot_thm =
-            instantiate' [SOME (Thm.global_ctyp_of thy ty)] [] @{thm identity_quotient}
+            instantiate' [SOME (Thm.ctyp_of ctxt ty)] [] @{thm identity_quotient}
         in
           (instantiated_id_quot_thm, (table, ctxt)) 
         end
@@ -388,10 +386,9 @@
         then (the (AList.lookup (op=) table ty), (table, ctxt))
         else 
           let
-            val thy = Proof_Context.theory_of ctxt
             val (Q_t, ctxt') = get_fresh_Q_t ctxt
-            val Q_thm = Thm.assume (Thm.global_cterm_of thy Q_t)
-            val table' = (ty, Q_thm)::table
+            val Q_thm = Thm.assume (Thm.cterm_of ctxt' Q_t)
+            val table' = (ty, Q_thm) :: table
           in
             (Q_thm, (table', ctxt'))
           end