# HG changeset patch
# User wenzelm
# Date 1559659625 -7200
# Node ID 24877d539fb89a4b238801a5f75de1996d403caa
# Parent  59258a3192bf12da2d4b3cc8b39ccd29055e35c0
proper context;

diff -r 59258a3192bf -r 24877d539fb8 src/HOL/Tools/Lifting/lifting_def_code_dt.ML
--- a/src/HOL/Tools/Lifting/lifting_def_code_dt.ML	Tue Jun 04 15:14:56 2019 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def_code_dt.ML	Tue Jun 04 16:47:05 2019 +0200
@@ -300,14 +300,14 @@
               EVERY' [Transfer.gen_frees_tac [] ctxt, DETERM o Transfer.transfer_tac true ctxt,
                 SELECT_GOAL (Local_Defs.unfold0_tac ctxt [id_apply]), rtac ctxt refl] i;
             val rep_isom_transfer = transfer_of_rep_isom_data rep_isom_data
-            val (_, transfer_ctxt) =
-              Proof_Context.note_thms ""
-                (Binding.empty_atts, [([rep_isom_transfer], [Transfer.transfer_add])]) args_ctxt
+            val (_, transfer_ctxt) = args_ctxt
+              |> Proof_Context.note_thms ""
+                  (Binding.empty_atts, [([rep_isom_transfer], [Transfer.transfer_add])])
             val f_alt_def =
               Goal.prove_sorry transfer_ctxt [] [] f_alt_def_goal
                 (fn {context = goal_ctxt, ...} => HEADGOAL (f_alt_def_tac goal_ctxt))
               |> Thm.close_derivation
-              |> singleton (Variable.export args_ctxt lthy4)  (* FIXME proper transfer_ctxt!? *)
+              |> singleton (Variable.export transfer_ctxt lthy4)
             val lthy5 = lthy4
               |> Local_Theory.note ((Binding.empty, @{attributes [code]}), [f_alt_def])
               |> snd
diff -r 59258a3192bf -r 24877d539fb8 src/HOL/Tools/Lifting/lifting_setup.ML
--- a/src/HOL/Tools/Lifting/lifting_setup.ML	Tue Jun 04 15:14:56 2019 +0200
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Tue Jun 04 16:47:05 2019 +0200
@@ -158,7 +158,7 @@
             |> Conv.fconv_rule (Conv.arg_conv (Conv.rewr_conv eq_OO_meta))
             |> HOLogic.mk_obj_eq
             |> singleton (Variable.export args_ctxt lthy)
-          val lthy' = args_ctxt  (* FIXME lthy!? *)
+          val lthy' = lthy
             |> #notes config ?
               (Local_Theory.note ((Binding.qualify_name true qty_name "pcr_cr_eq", []), [thm]) #> #2)
         in
diff -r 59258a3192bf -r 24877d539fb8 src/HOL/Tools/Lifting/lifting_term.ML
--- a/src/HOL/Tools/Lifting/lifting_term.ML	Tue Jun 04 15:14:56 2019 +0200
+++ b/src/HOL/Tools/Lifting/lifting_term.ML	Tue Jun 04 16:47:05 2019 +0200
@@ -456,8 +456,8 @@
       fun prove_extra_assms ctxt ctm distr_rule =
         let
           fun prove_assm assm =
-            try (Goal.prove ctxt [] [] (Thm.term_of assm)) (fn _ =>  (* FIXME proper goal_ctxt!? *)
-              SOLVED' (REPEAT_ALL_NEW (resolve_tac ctxt (Transfer.get_transfer_raw ctxt))) 1)
+            try (Goal.prove ctxt [] [] (Thm.term_of assm)) (fn {context = goal_ctxt, ...} =>
+              SOLVED' (REPEAT_ALL_NEW (resolve_tac goal_ctxt (Transfer.get_transfer_raw goal_ctxt))) 1)
   
           fun is_POS_or_NEG ctm =
             case (head_of o Thm.term_of o Thm.dest_arg) ctm of