--- 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
--- 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 *)