src/HOL/Tools/reification.ML
changeset 60696 8304fb4fb823
parent 60642 48dd1cefb4ae
child 60752 b48830b670a1
     1.1 --- a/src/HOL/Tools/reification.ML	Wed Jul 08 19:28:43 2015 +0200
     1.2 +++ b/src/HOL/Tools/reification.ML	Wed Jul 08 21:33:00 2015 +0200
     1.3 @@ -23,11 +23,12 @@
     1.4  
     1.5  val pure_subst = @{lemma "x == y ==> PROP P y ==> PROP P x" by simp}
     1.6  
     1.7 -fun lift_conv ctxt conv some_t = Subgoal.FOCUS (fn { concl, ... } =>
     1.8 +fun lift_conv ctxt conv some_t = Subgoal.FOCUS (fn {context = ctxt', concl, ...} =>
     1.9    let
    1.10 -    val ct = case some_t
    1.11 -     of NONE => Thm.dest_arg concl
    1.12 -      | SOME t => Thm.cterm_of ctxt t
    1.13 +    val ct =
    1.14 +      (case some_t of
    1.15 +        NONE => Thm.dest_arg concl
    1.16 +      | SOME t => Thm.cterm_of ctxt' t)
    1.17      val thm = conv ct;
    1.18    in
    1.19      if Thm.is_reflexive thm then no_tac