# HG changeset patch
# User wenzelm
# Date 1433845921 -7200
# Node ID 9be917b2f3767fd4f0d287c57e2ba6f1648ad97f
# Parent  2cfd1ead74c37fca69b8dbccf9dd452b7b942f21
tuned signature;

diff -r 2cfd1ead74c3 -r 9be917b2f376 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Tue Jun 09 12:17:50 2015 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Tue Jun 09 12:32:01 2015 +0200
@@ -187,7 +187,7 @@
 (* local endings *)
 
 fun local_qed m = Toplevel.proof (Proof.local_qed (m, true));
-val local_terminal_proof = Toplevel.proof' o Proof.local_future_terminal_proof;
+val local_terminal_proof = Toplevel.proof o Proof.local_future_terminal_proof;
 val local_default_proof = Toplevel.proof Proof.local_default_proof;
 val local_immediate_proof = Toplevel.proof Proof.local_immediate_proof;
 val local_done_proof = Toplevel.proof Proof.local_done_proof;
@@ -199,7 +199,7 @@
 (* global endings *)
 
 fun global_qed m = Toplevel.end_proof (K (Proof.global_qed (m, true)));
-val global_terminal_proof = Toplevel.end_proof o Proof.global_future_terminal_proof;
+val global_terminal_proof = Toplevel.end_proof o K o Proof.global_future_terminal_proof;
 val global_default_proof = Toplevel.end_proof (K Proof.global_default_proof);
 val global_immediate_proof = Toplevel.end_proof (K Proof.global_immediate_proof);
 val global_skip_proof = Toplevel.end_proof Proof.global_skip_proof;
diff -r 2cfd1ead74c3 -r 9be917b2f376 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Tue Jun 09 12:17:50 2015 +0200
+++ b/src/Pure/Isar/proof.ML	Tue Jun 09 12:32:01 2015 +0200
@@ -33,7 +33,7 @@
   val enter_chain: state -> state
   val enter_backward: state -> state
   val has_bottom_goal: state -> bool
-  val pretty_state: int -> state -> Pretty.T list
+  val pretty_state: state -> Pretty.T list
   val refine: Method.text -> state -> state Seq.seq
   val refine_end: Method.text -> state -> state Seq.seq
   val refine_insert: thm list -> state -> state
@@ -121,10 +121,8 @@
   val schematic_goal: state -> bool
   val is_relevant: state -> bool
   val future_proof: (state -> ('a * context) future) -> state -> 'a future * state
-  val local_future_terminal_proof: Method.text_range * Method.text_range option -> bool ->
-    state -> state
-  val global_future_terminal_proof: Method.text_range * Method.text_range option -> bool ->
-    state -> context
+  val local_future_terminal_proof: Method.text_range * Method.text_range option -> state -> state
+  val global_future_terminal_proof: Method.text_range * Method.text_range option -> state -> context
 end;
 
 structure Proof: PROOF =
@@ -362,13 +360,12 @@
 
 in
 
-fun pretty_state nr state =
+fun pretty_state state =
   let
     val {context = ctxt, facts, mode, goal = _} = top state;
     val verbose = Config.get ctxt Proof_Context.verbose;
 
-    fun prt_goal (SOME (_, (_,
-      {statement = ((_, pos), _, _), using, goal, before_qed = _, after_qed = _}))) =
+    fun prt_goal (SOME (_, (_, {statement = _, using, goal, before_qed = _, after_qed = _}))) =
           pretty_sep
             (pretty_facts ctxt "using"
               (if mode <> Backward orelse null using then NONE else SOME using))
@@ -1195,7 +1192,7 @@
 
 local
 
-fun future_terminal_proof proof1 proof2 done int state =
+fun future_terminal_proof proof1 proof2 done state =
   if Goal.future_enabled 3 andalso not (is_relevant state) then
     state |> future_proof (fn state' =>
       let
diff -r 2cfd1ead74c3 -r 9be917b2f376 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Tue Jun 09 12:17:50 2015 +0200
+++ b/src/Pure/Isar/toplevel.ML	Tue Jun 09 12:32:01 2015 +0200
@@ -192,8 +192,7 @@
   (case try node_of state of
     NONE => []
   | SOME (Theory _) => []
-  | SOME (Proof (prf, _)) =>
-      Proof.pretty_state (Proof_Node.position prf) (Proof_Node.current prf)
+  | SOME (Proof (prf, _)) => Proof.pretty_state (Proof_Node.current prf)
   | SOME (Skipped_Proof (d, _)) => [Pretty.str ("skipped proof: depth " ^ string_of_int d)]);
 
 val print_state = pretty_state #> Pretty.chunks #> Pretty.string_of #> Output.state;