# HG changeset patch
# User wenzelm
# Date 1208463741 -7200
# Node ID 3a478bfa165041f796fdc5f9f72438cd02d46d83
# Parent  f79aa228c582a1a13ad053a05bc16d0171149b12
prove_global: pass context;

diff -r f79aa228c582 -r 3a478bfa1650 src/HOL/Nominal/nominal_inductive.ML
--- a/src/HOL/Nominal/nominal_inductive.ML	Thu Apr 17 22:22:19 2008 +0200
+++ b/src/HOL/Nominal/nominal_inductive.ML	Thu Apr 17 22:22:21 2008 +0200
@@ -311,8 +311,7 @@
       in (freshs1 @ [term_of cx], freshs2 @ ths, ctxt') end;
 
     fun mk_ind_proof thy thss =
-      let val ctxt = ProofContext.init thy
-      in Goal.prove_global thy [] prems' concl' (fn ihyps =>
+      Goal.prove_global thy [] prems' concl' (fn {prems = ihyps, context = ctxt} =>
         let val th = Goal.prove ctxt [] [] concl (fn {context, ...} =>
           rtac raw_induct 1 THEN
           EVERY (maps (fn ((((_, bvars, oprems, _), vc_compat_ths), ihyp), (vs, ihypt)) =>
@@ -404,8 +403,7 @@
           REPEAT (REPEAT (resolve_tac [conjI, impI] 1) THEN
             etac impE 1 THEN atac 1 THEN REPEAT (etac allE_Nil 1) THEN
             asm_full_simp_tac (simpset_of thy) 1)
-        end)
-      end;
+        end);
 
     (** strong case analysis rule **)
 
@@ -460,8 +458,8 @@
 
     fun mk_cases_proof thy ((((name, thss), elim), (prem, args, concl, prems)),
         prems') =
-      let val ctxt1 = ProofContext.init thy
-      in (name, Goal.prove_global thy [] (prem :: prems') concl (fn hyp :: hyps =>
+      (name, Goal.prove_global thy [] (prem :: prems') concl
+        (fn {prems = hyp :: hyps, context = ctxt1} =>
         EVERY (rtac (hyp RS elim) 1 ::
           map (fn (((_, vc_compat_ths), case_hyp), (_, qs, is, _)) =>
             SUBPROOF (fn {prems = case_hyps, params, context = ctxt2, concl, ...} =>
@@ -534,7 +532,6 @@
                   val final = ProofContext.export ctxt3 ctxt2 [th]
                 in resolve_tac final 1 end) ctxt1 1)
                   (thss ~~ hyps ~~ prems))))
-      end
 
   in
     thy |>
diff -r f79aa228c582 -r 3a478bfa1650 src/HOL/Nominal/nominal_package.ML
--- a/src/HOL/Nominal/nominal_package.ML	Thu Apr 17 22:22:19 2008 +0200
+++ b/src/HOL/Nominal/nominal_package.ML	Thu Apr 17 22:22:21 2008 +0200
@@ -1049,7 +1049,7 @@
     val dt_induct_prop = DatatypeProp.make_ind descr' sorts';
     val dt_induct = Goal.prove_global thy8 []
       (Logic.strip_imp_prems dt_induct_prop) (Logic.strip_imp_concl dt_induct_prop)
-      (fn prems => EVERY
+      (fn {prems, ...} => EVERY
         [rtac indrule_lemma' 1,
          (indtac rep_induct [] THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1,
          EVERY (map (fn (prem, r) => (EVERY
@@ -1270,7 +1270,7 @@
 
     val _ = warning "proving strong induction theorem ...";
 
-    val induct_aux = Goal.prove_global thy9 [] ind_prems' ind_concl' (fn prems =>
+    val induct_aux = Goal.prove_global thy9 [] ind_prems' ind_concl' (fn {prems, context} =>
       let
         val (prems1, prems2) = chop (length dt_atomTs) prems;
         val ind_ss2 = HOL_ss addsimps
@@ -1283,7 +1283,7 @@
           fin_set_fresh @ calc_atm;
         val ind_ss5 = HOL_basic_ss addsimps pt1_atoms;
         val ind_ss6 = HOL_basic_ss addsimps flat perm_simps';
-        val th = Goal.prove (ProofContext.init thy9) [] [] aux_ind_concl
+        val th = Goal.prove context [] [] aux_ind_concl
           (fn {context = context1, ...} =>
              EVERY (indtac dt_induct tnames 1 ::
                maps (fn ((_, (_, _, constrs)), (_, constrs')) =>
@@ -1369,7 +1369,7 @@
         end) fresh_fs) induct_aux;
 
     val induct = Goal.prove_global thy9 [] ind_prems ind_concl
-      (fn prems => EVERY
+      (fn {prems, ...} => EVERY
          [rtac induct_aux' 1,
           REPEAT (resolve_tac fs_atoms 1),
           REPEAT ((resolve_tac prems THEN_ALL_NEW
@@ -1552,7 +1552,8 @@
                    HOLogic.mk_imp (R $ x $ y,
                      finite $ (Const ("Nominal.supp", U --> aset) $ y))
                  end) (recTs ~~ rec_result_Ts ~~ rec_sets ~~ (1 upto length recTs)))))
-            (fn fins => (rtac rec_induct THEN_ALL_NEW cut_facts_tac fins) 1 THEN REPEAT
+            (fn {prems = fins, ...} =>
+              (rtac rec_induct THEN_ALL_NEW cut_facts_tac fins) 1 THEN REPEAT
                (NominalPermeq.finite_guess_tac (HOL_ss addsimps [fs_name]) 1))))
       end) dt_atomTs;
 
@@ -1992,7 +1993,7 @@
           (resolve_tac prems THEN_ALL_NEW atac)
       in
         Goal.prove_global thy12 [] prems' concl'
-          (fn prems => EVERY
+          (fn {prems, ...} => EVERY
             [rewrite_goals_tac reccomb_defs,
              rtac the1_equality 1,
              solve rec_unique_thms prems 1,
diff -r f79aa228c582 -r 3a478bfa1650 src/HOL/Tools/datatype_abs_proofs.ML
--- a/src/HOL/Tools/datatype_abs_proofs.ML	Thu Apr 17 22:22:19 2008 +0200
+++ b/src/HOL/Tools/datatype_abs_proofs.ML	Thu Apr 17 22:22:21 2008 +0200
@@ -71,7 +71,7 @@
 
       in
         SkipProof.prove_global thy [] (Logic.strip_imp_prems t) (Logic.strip_imp_concl t)
-          (fn prems => EVERY
+          (fn {prems, ...} => EVERY
             [rtac induct' 1,
              REPEAT (rtac TrueI 1),
              REPEAT ((rtac impI 1) THEN (eresolve_tac prems 1)),
@@ -383,7 +383,7 @@
   let
     fun prove_weak_case_cong t =
        SkipProof.prove_global thy [] (Logic.strip_imp_prems t) (Logic.strip_imp_concl t)
-         (fn prems => EVERY [rtac ((hd prems) RS arg_cong) 1])
+         (fn {prems, ...} => EVERY [rtac ((hd prems) RS arg_cong) 1])
 
     val weak_case_congs = map prove_weak_case_cong (DatatypeProp.make_weak_case_congs
       new_type_names descr sorts thy)
@@ -426,7 +426,7 @@
           [(cert (hd (add_term_vars (concl_of nchotomy', []))), cert Ma)] nchotomy'
       in
         SkipProof.prove_global thy [] (Logic.strip_imp_prems t) (Logic.strip_imp_concl t)
-          (fn prems => 
+          (fn {prems, ...} => 
             let val simplify = asm_simp_tac (HOL_ss addsimps (prems @ case_rewrites))
             in EVERY [simp_tac (HOL_ss addsimps [hd prems]) 1,
                 cut_facts_tac [nchotomy''] 1,
diff -r f79aa228c582 -r 3a478bfa1650 src/HOL/Tools/datatype_rep_proofs.ML
--- a/src/HOL/Tools/datatype_rep_proofs.ML	Thu Apr 17 22:22:19 2008 +0200
+++ b/src/HOL/Tools/datatype_rep_proofs.ML	Thu Apr 17 22:22:21 2008 +0200
@@ -607,7 +607,7 @@
     val dt_induct_prop = DatatypeProp.make_ind descr sorts;
     val dt_induct = SkipProof.prove_global thy6 []
       (Logic.strip_imp_prems dt_induct_prop) (Logic.strip_imp_concl dt_induct_prop)
-      (fn prems => EVERY
+      (fn {prems, ...} => EVERY
         [rtac indrule_lemma' 1,
          (indtac rep_induct [] THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1,
          EVERY (map (fn (prem, r) => (EVERY
diff -r f79aa228c582 -r 3a478bfa1650 src/HOL/Tools/inductive_realizer.ML
--- a/src/HOL/Tools/inductive_realizer.ML	Thu Apr 17 22:22:19 2008 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML	Thu Apr 17 22:22:21 2008 +0200
@@ -391,7 +391,7 @@
           (fn (_, _ $ P, _ $ Q) => HOLogic.mk_imp (P, Q)) rlzs'));
         val rews = map mk_meta_eq
           (fst_conv :: snd_conv :: get #rec_thms dt_info);
-        val thm = Goal.prove_global thy [] prems concl (fn prems => EVERY
+        val thm = Goal.prove_global thy [] prems concl (fn {prems, ...} => EVERY
           [rtac (#raw_induct ind_info) 1,
            rewrite_goals_tac rews,
            REPEAT ((resolve_tac prems THEN_ALL_NEW EVERY'
@@ -450,7 +450,7 @@
         val rlz' = strip_all (Logic.unvarify rlz);
         val rews = map mk_meta_eq case_thms;
         val thm = Goal.prove_global thy []
-          (Logic.strip_imp_prems rlz') (Logic.strip_imp_concl rlz') (fn prems => EVERY
+          (Logic.strip_imp_prems rlz') (Logic.strip_imp_concl rlz') (fn {prems, ...} => EVERY
           [cut_facts_tac [hd prems] 1,
            etac elimR 1,
            ALLGOALS (asm_simp_tac HOL_basic_ss),
diff -r f79aa228c582 -r 3a478bfa1650 src/HOL/simpdata.ML
--- a/src/HOL/simpdata.ML	Thu Apr 17 22:22:19 2008 +0200
+++ b/src/HOL/simpdata.ML	Thu Apr 17 22:22:21 2008 +0200
@@ -73,7 +73,7 @@
       in Goal.prove_global (Thm.theory_of_thm st) []
         [mk_simp_implies (Logic.mk_equals (x, y))]
         (mk_simp_implies (HOLogic.mk_Trueprop (HOLogic.mk_eq (x, y))))
-        (fn prems => EVERY
+        (fn {prems, ...} => EVERY
          [rewrite_goals_tac @{thms simp_implies_def},
           REPEAT (ares_tac (@{thm meta_eq_to_obj_eq} ::
             map (rewrite_rule @{thms simp_implies_def}) prems) 1)])
diff -r f79aa228c582 -r 3a478bfa1650 src/HOLCF/Tools/domain/domain_theorems.ML
--- a/src/HOLCF/Tools/domain/domain_theorems.ML	Thu Apr 17 22:22:19 2008 +0200
+++ b/src/HOLCF/Tools/domain/domain_theorems.ML	Thu Apr 17 22:22:21 2008 +0200
@@ -84,7 +84,7 @@
     val t' = legacy_infer_term thy t;
     val asms = Logic.strip_imp_prems t';
     val prop = Logic.strip_imp_concl t';
-    fun tac prems =
+    fun tac {prems, context} =
       rewrite_goals_tac defs THEN
       EVERY (tacs (map (rewrite_rule defs) prems));
   in Goal.prove_global thy [] asms prop tac end;
diff -r f79aa228c582 -r 3a478bfa1650 src/Provers/splitter.ML
--- a/src/Provers/splitter.ML	Thu Apr 17 22:22:19 2008 +0200
+++ b/src/Provers/splitter.ML	Thu Apr 17 22:22:21 2008 +0200
@@ -105,7 +105,7 @@
 val lift = Goal.prove_global Pure.thy ["P", "Q", "R"]
   [Syntax.read_prop_global Pure.thy "!!x :: 'b. Q(x) == R(x) :: 'c"]
   (Syntax.read_prop_global Pure.thy "P(%x. Q(x)) == P(%x. R(x))")
-  (fn [prem] => rewtac prem THEN rtac reflexive_thm 1)
+  (fn {prems = [prem], ...} => rewtac prem THEN rtac reflexive_thm 1)
 
 val trlift = lift RS transitive_thm;
 val _ $ (P $ _) $ _ = concl_of trlift;
diff -r f79aa228c582 -r 3a478bfa1650 src/Pure/Isar/skip_proof.ML
--- a/src/Pure/Isar/skip_proof.ML	Thu Apr 17 22:22:19 2008 +0200
+++ b/src/Pure/Isar/skip_proof.ML	Thu Apr 17 22:22:21 2008 +0200
@@ -12,7 +12,7 @@
   val prove: Proof.context -> string list -> term list -> term ->
     ({prems: thm list, context: Proof.context} -> tactic) -> thm
   val prove_global: theory -> string list -> term list -> term ->
-    (thm list -> tactic) -> thm
+    ({prems: thm list, context: Proof.context} -> tactic) -> thm
 end;
 
 structure SkipProof: SKIP_PROOF =
@@ -45,6 +45,6 @@
     else tac args st);
 
 fun prove_global thy xs asms prop tac =
-  Drule.standard (prove (ProofContext.init thy) xs asms prop (fn {prems, ...} => tac prems));
+  Drule.standard (prove (ProofContext.init thy) xs asms prop tac);
 
 end;