--- 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
--- 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
--- 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