# HG changeset patch
# User wenzelm
# Date 1154127089 -7200
# Node ID 7916ce5bb06951aad7560e4a2d6d2f99f300f8c4
# Parent  32fb8d2715de0fba3591bbf119dbc7646c38e62f
Goal.prove: more tactic arguments;

diff -r 32fb8d2715de -r 7916ce5bb069 src/HOL/Tools/inductive_package.ML
--- a/src/HOL/Tools/inductive_package.ML	Fri Jul 28 18:37:25 2006 +0200
+++ b/src/HOL/Tools/inductive_package.ML	Sat Jul 29 00:51:29 2006 +0200
@@ -507,7 +507,7 @@
   in
     mk_elims cs cTs params intr_ts intr_names |> map (fn (t, cases) =>
       SkipProof.prove ctxt [] (Logic.strip_imp_prems t) (Logic.strip_imp_concl t)
-        (fn prems => EVERY
+        (fn {prems, ...} => EVERY
           [cut_facts_tac [hd prems] 1,
            rewrite_goals_tac rec_sets_defs,
            dtac (unfold RS subst) 1,
@@ -653,7 +653,7 @@
             else ();
 
     val induct = standard (SkipProof.prove ctxt [] ind_prems ind_concl
-      (fn prems => EVERY
+      (fn {prems, ...} => EVERY
         [rewrite_goals_tac [inductive_conj_def],
          rtac (impI RS allI) 1,
          DETERM (etac raw_fp_induct 1),
diff -r 32fb8d2715de -r 7916ce5bb069 src/HOL/Tools/record_package.ML
--- a/src/HOL/Tools/record_package.ML	Fri Jul 28 18:37:25 2006 +0200
+++ b/src/HOL/Tools/record_package.ML	Sat Jul 29 00:51:29 2006 +0200
@@ -1438,7 +1438,7 @@
 
     fun induct_prf () =
       let val (assm, concl) = induct_prop
-      in prove_standard [assm] concl (fn prems =>
+      in prove_standard [assm] concl (fn {prems, ...} =>
            EVERY [try_param_tac rN abs_induct 1,
                   simp_tac (HOL_ss addsimps [split_paired_all]) 1,
                   resolve_tac (map (rewrite_rule [ext_def]) prems) 1])
@@ -1878,7 +1878,7 @@
     fun induct_prf () =
       let val (assm, concl) = induct_prop;
       in
-        prove_standard [assm] concl (fn prems =>
+        prove_standard [assm] concl (fn {prems, ...} =>
           try_param_tac rN induct_scheme 1
           THEN try_param_tac "more" unit_induct 1
           THEN resolve_tac prems 1)
diff -r 32fb8d2715de -r 7916ce5bb069 src/Pure/Isar/skip_proof.ML
--- a/src/Pure/Isar/skip_proof.ML	Fri Jul 28 18:37:25 2006 +0200
+++ b/src/Pure/Isar/skip_proof.ML	Sat Jul 29 00:51:29 2006 +0200
@@ -9,8 +9,8 @@
 sig
   val make_thm: theory -> term -> thm
   val cheat_tac: theory -> tactic
-  val prove: ProofContext.context ->
-    string list -> term list -> term -> (thm list -> tactic) -> thm
+  val prove: ProofContext.context -> string list -> term list -> term ->
+    ({prems: thm list, context: Context.proof} -> tactic) -> thm
 end;
 
 structure SkipProof: SKIP_PROOF =