proper context;
authorwenzelm
Tue Jun 04 16:47:05 2019 +0200 (6 weeks ago)
changeset 7032124877d539fb8
parent 70320 59258a3192bf
child 70322 65b880d4efbb
proper context;
src/HOL/Tools/Lifting/lifting_def_code_dt.ML
src/HOL/Tools/Lifting/lifting_setup.ML
src/HOL/Tools/Lifting/lifting_term.ML
     1.1 --- a/src/HOL/Tools/Lifting/lifting_def_code_dt.ML	Tue Jun 04 15:14:56 2019 +0200
     1.2 +++ b/src/HOL/Tools/Lifting/lifting_def_code_dt.ML	Tue Jun 04 16:47:05 2019 +0200
     1.3 @@ -300,14 +300,14 @@
     1.4                EVERY' [Transfer.gen_frees_tac [] ctxt, DETERM o Transfer.transfer_tac true ctxt,
     1.5                  SELECT_GOAL (Local_Defs.unfold0_tac ctxt [id_apply]), rtac ctxt refl] i;
     1.6              val rep_isom_transfer = transfer_of_rep_isom_data rep_isom_data
     1.7 -            val (_, transfer_ctxt) =
     1.8 -              Proof_Context.note_thms ""
     1.9 -                (Binding.empty_atts, [([rep_isom_transfer], [Transfer.transfer_add])]) args_ctxt
    1.10 +            val (_, transfer_ctxt) = args_ctxt
    1.11 +              |> Proof_Context.note_thms ""
    1.12 +                  (Binding.empty_atts, [([rep_isom_transfer], [Transfer.transfer_add])])
    1.13              val f_alt_def =
    1.14                Goal.prove_sorry transfer_ctxt [] [] f_alt_def_goal
    1.15                  (fn {context = goal_ctxt, ...} => HEADGOAL (f_alt_def_tac goal_ctxt))
    1.16                |> Thm.close_derivation
    1.17 -              |> singleton (Variable.export args_ctxt lthy4)  (* FIXME proper transfer_ctxt!? *)
    1.18 +              |> singleton (Variable.export transfer_ctxt lthy4)
    1.19              val lthy5 = lthy4
    1.20                |> Local_Theory.note ((Binding.empty, @{attributes [code]}), [f_alt_def])
    1.21                |> snd
     2.1 --- a/src/HOL/Tools/Lifting/lifting_setup.ML	Tue Jun 04 15:14:56 2019 +0200
     2.2 +++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Tue Jun 04 16:47:05 2019 +0200
     2.3 @@ -158,7 +158,7 @@
     2.4              |> Conv.fconv_rule (Conv.arg_conv (Conv.rewr_conv eq_OO_meta))
     2.5              |> HOLogic.mk_obj_eq
     2.6              |> singleton (Variable.export args_ctxt lthy)
     2.7 -          val lthy' = args_ctxt  (* FIXME lthy!? *)
     2.8 +          val lthy' = lthy
     2.9              |> #notes config ?
    2.10                (Local_Theory.note ((Binding.qualify_name true qty_name "pcr_cr_eq", []), [thm]) #> #2)
    2.11          in
     3.1 --- a/src/HOL/Tools/Lifting/lifting_term.ML	Tue Jun 04 15:14:56 2019 +0200
     3.2 +++ b/src/HOL/Tools/Lifting/lifting_term.ML	Tue Jun 04 16:47:05 2019 +0200
     3.3 @@ -456,8 +456,8 @@
     3.4        fun prove_extra_assms ctxt ctm distr_rule =
     3.5          let
     3.6            fun prove_assm assm =
     3.7 -            try (Goal.prove ctxt [] [] (Thm.term_of assm)) (fn _ =>  (* FIXME proper goal_ctxt!? *)
     3.8 -              SOLVED' (REPEAT_ALL_NEW (resolve_tac ctxt (Transfer.get_transfer_raw ctxt))) 1)
     3.9 +            try (Goal.prove ctxt [] [] (Thm.term_of assm)) (fn {context = goal_ctxt, ...} =>
    3.10 +              SOLVED' (REPEAT_ALL_NEW (resolve_tac goal_ctxt (Transfer.get_transfer_raw goal_ctxt))) 1)
    3.11    
    3.12            fun is_POS_or_NEG ctm =
    3.13              case (head_of o Thm.term_of o Thm.dest_arg) ctm of