# HG changeset patch
# User wenzelm
# Date 1433684149 -7200
# Node ID 26dcc7f19b02b0320f43bc0de7e7097eb89f5529
# Parent  234b7da8542eb905e24730fa3f157a6c3616c1a9
tuned signature;

diff -r 234b7da8542e -r 26dcc7f19b02 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Sun Jun 07 15:01:07 2015 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Sun Jun 07 15:35:49 2015 +0200
@@ -20,10 +20,6 @@
   val declaration: {syntax: bool, pervasive: bool} -> Input.source -> local_theory -> local_theory
   val simproc_setup: string * Position.T -> string list -> Input.source ->
     string list -> local_theory -> local_theory
-  val have: (Attrib.binding * (string * string list) list) list -> bool -> Proof.state -> Proof.state
-  val hence: (Attrib.binding * (string * string list) list) list -> bool -> Proof.state -> Proof.state
-  val show: (Attrib.binding * (string * string list) list) list -> bool -> Proof.state -> Proof.state
-  val thus: (Attrib.binding * (string * string list) list) list -> bool -> Proof.state -> Proof.state
   val qed: Method.text_range option -> Toplevel.transition -> Toplevel.transition
   val terminal_proof: Method.text_range * Method.text_range option ->
     Toplevel.transition -> Toplevel.transition
diff -r 234b7da8542e -r 26dcc7f19b02 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Sun Jun 07 15:01:07 2015 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Sun Jun 07 15:35:49 2015 +0200
@@ -490,20 +490,22 @@
 
 val _ =
   Outer_Syntax.command @{command_keyword have} "state local goal"
-    (Parse_Spec.statement >> (Toplevel.proof' o Isar_Cmd.have));
+    (Parse_Spec.statement >> (Toplevel.proof' o Proof.have_cmd NONE (K I)));
 
 val _ =
   Outer_Syntax.command @{command_keyword hence} "old-style alias of \"then have\""
-    (Parse_Spec.statement >> (Toplevel.proof' o Isar_Cmd.hence));
+    (Parse_Spec.statement >> (fn stmt =>
+      Toplevel.proof' (fn int => Proof.chain #> Proof.have_cmd NONE (K I) stmt int)));
 
 val _ =
   Outer_Syntax.command @{command_keyword show}
     "state local goal, solving current obligation"
-    (Parse_Spec.statement >> (Toplevel.proof' o Isar_Cmd.show));
+    (Parse_Spec.statement >> (Toplevel.proof' o Proof.show_cmd NONE (K I)));
 
 val _ =
   Outer_Syntax.command @{command_keyword thus} "old-style alias of  \"then show\""
-    (Parse_Spec.statement >> (Toplevel.proof' o Isar_Cmd.thus));
+    (Parse_Spec.statement >> (fn stmt =>
+      Toplevel.proof' (fn int => Proof.chain #> Proof.show_cmd NONE (K I) stmt int)));
 
 
 (* facts *)