src/HOL/Nominal/nominal_inductive.ML
changeset 59498 50b60f501b05
parent 59058 a78612c67ec0
child 59582 0fbed69ff081
     1.1 --- a/src/HOL/Nominal/nominal_inductive.ML	Tue Feb 10 14:29:36 2015 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_inductive.ML	Tue Feb 10 14:48:26 2015 +0100
     1.3 @@ -130,7 +130,7 @@
     1.4      fun prove t =
     1.5        Goal.prove ctxt [] [] t (fn _ =>
     1.6          EVERY [cut_facts_tac [th] 1, etac rev_mp 1,
     1.7 -          REPEAT_DETERM (FIRSTGOAL (resolve_tac monos)),
     1.8 +          REPEAT_DETERM (FIRSTGOAL (resolve_tac ctxt monos)),
     1.9            REPEAT_DETERM (rtac impI 1 THEN (atac 1 ORELSE tac))])
    1.10    in Option.map prove (map_term f prop (the_default prop opt)) end;
    1.11  
    1.12 @@ -296,8 +296,8 @@
    1.13                NominalDatatype.fresh_const T (fastype_of p) $
    1.14                  Bound 0 $ p)))
    1.15            (fn _ => EVERY
    1.16 -            [resolve_tac exists_fresh' 1,
    1.17 -             resolve_tac fs_atoms 1]);
    1.18 +            [resolve_tac ctxt exists_fresh' 1,
    1.19 +             resolve_tac ctxt fs_atoms 1]);
    1.20          val (([(_, cx)], ths), ctxt') = Obtain.result
    1.21            (fn ctxt' => EVERY
    1.22              [etac exE 1,
    1.23 @@ -388,17 +388,17 @@
    1.24                         (simp_tac (put_simpset HOL_basic_ss ctxt''
    1.25                            addsimps [inductive_forall_def']
    1.26                            addsimprocs [NominalDatatype.perm_simproc]) 1 THEN
    1.27 -                        resolve_tac gprems2 1)]));
    1.28 +                        resolve_tac ctxt'' gprems2 1)]));
    1.29                   val final = Goal.prove ctxt'' [] [] (term_of concl)
    1.30                     (fn _ => cut_facts_tac [th] 1 THEN full_simp_tac (put_simpset HOL_ss ctxt''
    1.31                       addsimps vc_compat_ths'' @ freshs2' @
    1.32                         perm_fresh_fresh @ fresh_atm) 1);
    1.33                   val final' = Proof_Context.export ctxt'' ctxt' [final];
    1.34 -               in resolve_tac final' 1 end) context 1])
    1.35 +               in resolve_tac ctxt' final' 1 end) context 1])
    1.36                   (prems ~~ thss ~~ ihyps ~~ prems'')))
    1.37          in
    1.38            cut_facts_tac [th] 1 THEN REPEAT (etac conjE 1) THEN
    1.39 -          REPEAT (REPEAT (resolve_tac [conjI, impI] 1) THEN
    1.40 +          REPEAT (REPEAT (resolve_tac ctxt [conjI, impI] 1) THEN
    1.41              etac impE 1 THEN atac 1 THEN REPEAT (etac @{thm allE_Nil} 1) THEN
    1.42              asm_full_simp_tac ctxt 1)
    1.43          end) |> singleton (Proof_Context.export ctxt' ctxt);
    1.44 @@ -532,10 +532,10 @@
    1.45                           in
    1.46                             simp_tac case_simpset 1 THEN
    1.47                             REPEAT_DETERM (TRY (rtac conjI 1) THEN
    1.48 -                             resolve_tac case_hyps' 1)
    1.49 +                             resolve_tac ctxt4 case_hyps' 1)
    1.50                           end) ctxt4 1)
    1.51                    val final = Proof_Context.export ctxt3 ctxt2 [th]
    1.52 -                in resolve_tac final 1 end) ctxt1 1)
    1.53 +                in resolve_tac ctxt2 final 1 end) ctxt1 1)
    1.54                    (thss ~~ hyps ~~ prems))) |>
    1.55                    singleton (Proof_Context.export ctxt' ctxt))
    1.56  
    1.57 @@ -634,7 +634,7 @@
    1.58              val intr' = Drule.cterm_instantiate (map (cterm_of thy) vs ~~
    1.59                 map (cterm_of thy o NominalDatatype.mk_perm [] pi o term_of o #2) params)
    1.60                 intr
    1.61 -          in (rtac intr' THEN_ALL_NEW (TRY o resolve_tac prems'')) 1
    1.62 +          in (rtac intr' THEN_ALL_NEW (TRY o resolve_tac ctxt'' prems'')) 1
    1.63            end) ctxt' 1 st
    1.64        in
    1.65          case (Seq.pull res handle THM (s, _, _) => eqvt_err s) of