src/HOL/NSA/transfer.ML
changeset 58957 c9e744ea8a38
parent 58825 2065f49da190
child 59498 50b60f501b05
     1.1 --- a/src/HOL/NSA/transfer.ML	Sun Nov 09 14:08:00 2014 +0100
     1.2 +++ b/src/HOL/NSA/transfer.ML	Sun Nov 09 17:04:14 2014 +0100
     1.3 @@ -62,10 +62,10 @@
     1.4      val tac =
     1.5        rewrite_goals_tac ctxt (ths' @ refolds' @ unfolds') THEN
     1.6        ALLGOALS (Object_Logic.full_atomize_tac ctxt) THEN
     1.7 -      match_tac [transitive_thm] 1 THEN
     1.8 +      match_tac ctxt [transitive_thm] 1 THEN
     1.9        resolve_tac [@{thm transfer_start}] 1 THEN
    1.10        REPEAT_ALL_NEW (resolve_tac intros) 1 THEN
    1.11 -      match_tac [reflexive_thm] 1
    1.12 +      match_tac ctxt [reflexive_thm] 1
    1.13    in Goal.prove ctxt [] [] (Logic.mk_equals (t,u)) (K tac) end
    1.14  
    1.15  fun transfer_tac ctxt ths =