# HG changeset patch
# User wenzelm
# Date 1372240485 -7200
# Node ID 960202346d0c6990b0a20df959b51aa513c703c5
# Parent  9a8f4fdac3cff10b26e9fbe45447008df534d72b
tuned signature;

diff -r 9a8f4fdac3cf -r 960202346d0c src/Doc/IsarImplementation/Tactic.thy
--- a/src/Doc/IsarImplementation/Tactic.thy	Wed Jun 26 09:58:39 2013 +0200
+++ b/src/Doc/IsarImplementation/Tactic.thy	Wed Jun 26 11:54:45 2013 +0200
@@ -53,8 +53,10 @@
   with protected propositions:
 
   \[
-  \infer[@{text "(protect)"}]{@{text "#C"}}{@{text "C"}} \qquad
-  \infer[@{text "(conclude)"}]{@{text "A\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^sub>n \<Longrightarrow> C"}}{@{text "A\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^sub>n \<Longrightarrow> #C"}}
+  \infer[@{text "(protect n)"}]{@{text "A\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^sub>n \<Longrightarrow> #C"}}{@{text "A\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^sub>n \<Longrightarrow> C"}}
+  \]
+  \[
+  \infer[@{text "(conclude)"}]{@{text "A \<Longrightarrow> \<dots> \<Longrightarrow> C"}}{@{text "A \<Longrightarrow> \<dots> \<Longrightarrow> #C"}}
   \]
 *}
 
@@ -62,7 +64,7 @@
   \begin{mldecls}
   @{index_ML Goal.init: "cterm -> thm"} \\
   @{index_ML Goal.finish: "Proof.context -> thm -> thm"} \\
-  @{index_ML Goal.protect: "thm -> thm"} \\
+  @{index_ML Goal.protect: "int -> thm -> thm"} \\
   @{index_ML Goal.conclude: "thm -> thm"} \\
   \end{mldecls}
 
@@ -76,8 +78,9 @@
   result by removing the goal protection.  The context is only
   required for printing error messages.
 
-  \item @{ML "Goal.protect"}~@{text "thm"} protects the full statement
-  of theorem @{text "thm"}.
+  \item @{ML "Goal.protect"}~@{text "n thm"} protects the statement
+  of theorem @{text "thm"}.  The parameter @{text n} indicates the
+  number of premises to be retained.
 
   \item @{ML "Goal.conclude"}~@{text "thm"} removes the goal
   protection, even if there are pending subgoals.
diff -r 9a8f4fdac3cf -r 960202346d0c src/HOL/Tools/Function/function_core.ML
--- a/src/HOL/Tools/Function/function_core.ML	Wed Jun 26 09:58:39 2013 +0200
+++ b/src/HOL/Tools/Function/function_core.ML	Wed Jun 26 11:54:45 2013 +0200
@@ -425,7 +425,7 @@
 
     val goalstate =  Conjunction.intr graph_is_function complete
       |> Thm.close_derivation
-      |> Goal.protect
+      |> Goal.protect 0
       |> fold_rev (Thm.implies_intr o cprop_of) compat
       |> Thm.implies_intr (cprop_of complete)
   in
diff -r 9a8f4fdac3cf -r 960202346d0c src/Pure/Isar/obtain.ML
--- a/src/Pure/Isar/obtain.ML	Wed Jun 26 09:58:39 2013 +0200
+++ b/src/Pure/Isar/obtain.ML	Wed Jun 26 11:54:45 2013 +0200
@@ -301,7 +301,7 @@
     fun print_result ctxt' (k, [(s, [_, th])]) =
       Proof_Display.print_results Markup.state int ctxt' (k, [(s, [th])]);
     val before_qed = SOME (Method.primitive_text (Goal.conclude #> Raw_Simplifier.norm_hhf #>
-        (fn th => Goal.protect (Conjunction.intr (Drule.mk_term (Thm.cprop_of th)) th))));
+        (fn th => Goal.protect 0 (Conjunction.intr (Drule.mk_term (Thm.cprop_of th)) th))));
     fun after_qed [[_, res]] =
       Proof.end_block #> guess_context (check_result ctxt thesis res);
   in
diff -r 9a8f4fdac3cf -r 960202346d0c src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Wed Jun 26 09:58:39 2013 +0200
+++ b/src/Pure/Isar/proof.ML	Wed Jun 26 11:54:45 2013 +0200
@@ -1133,8 +1133,7 @@
 
     val prop' = Logic.protect prop;
     val statement' = (kind, [[], [prop']], prop');
-    val goal' = Thm.adjust_maxidx_thm (Thm.maxidx_of goal)
-      (Drule.comp_no_flatten (goal, Thm.nprems_of goal) 1 Drule.protectI);
+    val goal' = Thm.adjust_maxidx_thm (Thm.maxidx_of goal) (Goal.protect (Thm.nprems_of goal) goal);
     val after_qed' = (fn [[th]] => map_context (set_result th), fn [[th]] => set_result th);
 
     val result_ctxt =
diff -r 9a8f4fdac3cf -r 960202346d0c src/Pure/goal.ML
--- a/src/Pure/goal.ML	Wed Jun 26 09:58:39 2013 +0200
+++ b/src/Pure/goal.ML	Wed Jun 26 11:54:45 2013 +0200
@@ -19,7 +19,7 @@
 sig
   include BASIC_GOAL
   val init: cterm -> thm
-  val protect: thm -> thm
+  val protect: int -> thm -> thm
   val conclude: thm -> thm
   val check_finished: Proof.context -> thm -> thm
   val finish: Proof.context -> thm -> thm
@@ -73,11 +73,11 @@
   in fn C => Thm.instantiate ([], [(A, C)]) Drule.protectI end;
 
 (*
-   C
-  --- (protect)
-  #C
+  A1 ==> ... ==> An ==> C
+  ------------------------ (protect n)
+  A1 ==> ... ==> An ==> #C
 *)
-fun protect th = Drule.comp_no_flatten (th, 0) 1 Drule.protectI;
+fun protect n th = Drule.comp_no_flatten (th, n) 1 Drule.protectI;
 
 (*
   A ==> ... ==> #C