tuned signature;
authorwenzelm
Sun Jun 07 15:35:49 2015 +0200 (2015-06-07 ago)
changeset 6037826dcc7f19b02
parent 60377 234b7da8542e
child 60379 51d9dcd71ad7
tuned signature;
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/isar_syn.ML
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Sun Jun 07 15:01:07 2015 +0200
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Sun Jun 07 15:35:49 2015 +0200
     1.3 @@ -20,10 +20,6 @@
     1.4    val declaration: {syntax: bool, pervasive: bool} -> Input.source -> local_theory -> local_theory
     1.5    val simproc_setup: string * Position.T -> string list -> Input.source ->
     1.6      string list -> local_theory -> local_theory
     1.7 -  val have: (Attrib.binding * (string * string list) list) list -> bool -> Proof.state -> Proof.state
     1.8 -  val hence: (Attrib.binding * (string * string list) list) list -> bool -> Proof.state -> Proof.state
     1.9 -  val show: (Attrib.binding * (string * string list) list) list -> bool -> Proof.state -> Proof.state
    1.10 -  val thus: (Attrib.binding * (string * string list) list) list -> bool -> Proof.state -> Proof.state
    1.11    val qed: Method.text_range option -> Toplevel.transition -> Toplevel.transition
    1.12    val terminal_proof: Method.text_range * Method.text_range option ->
    1.13      Toplevel.transition -> Toplevel.transition
     2.1 --- a/src/Pure/Isar/isar_syn.ML	Sun Jun 07 15:01:07 2015 +0200
     2.2 +++ b/src/Pure/Isar/isar_syn.ML	Sun Jun 07 15:35:49 2015 +0200
     2.3 @@ -490,20 +490,22 @@
     2.4  
     2.5  val _ =
     2.6    Outer_Syntax.command @{command_keyword have} "state local goal"
     2.7 -    (Parse_Spec.statement >> (Toplevel.proof' o Isar_Cmd.have));
     2.8 +    (Parse_Spec.statement >> (Toplevel.proof' o Proof.have_cmd NONE (K I)));
     2.9  
    2.10  val _ =
    2.11    Outer_Syntax.command @{command_keyword hence} "old-style alias of \"then have\""
    2.12 -    (Parse_Spec.statement >> (Toplevel.proof' o Isar_Cmd.hence));
    2.13 +    (Parse_Spec.statement >> (fn stmt =>
    2.14 +      Toplevel.proof' (fn int => Proof.chain #> Proof.have_cmd NONE (K I) stmt int)));
    2.15  
    2.16  val _ =
    2.17    Outer_Syntax.command @{command_keyword show}
    2.18      "state local goal, solving current obligation"
    2.19 -    (Parse_Spec.statement >> (Toplevel.proof' o Isar_Cmd.show));
    2.20 +    (Parse_Spec.statement >> (Toplevel.proof' o Proof.show_cmd NONE (K I)));
    2.21  
    2.22  val _ =
    2.23    Outer_Syntax.command @{command_keyword thus} "old-style alias of  \"then show\""
    2.24 -    (Parse_Spec.statement >> (Toplevel.proof' o Isar_Cmd.thus));
    2.25 +    (Parse_Spec.statement >> (fn stmt =>
    2.26 +      Toplevel.proof' (fn int => Proof.chain #> Proof.show_cmd NONE (K I) stmt int)));
    2.27  
    2.28  
    2.29  (* facts *)