1.1 --- a/src/Pure/Isar/expression.ML	Tue Apr 03 10:59:20 2012 +0200
     1.2 +++ b/src/Pure/Isar/expression.ML	Tue Apr 03 11:21:17 2012 +0200
     1.3 @@ -43,12 +43,9 @@
     1.4      (Attrib.binding * term) list -> theory -> Proof.state
     1.5    val sublocale_cmd: (local_theory -> local_theory) -> xstring * Position.T -> expression ->
     1.6      (Attrib.binding * string) list -> theory -> Proof.state
     1.7 -  val interpretation: expression_i -> (Attrib.binding * term) list ->
     1.8 -    theory -> Proof.state
     1.9 -  val interpretation_cmd: expression -> (Attrib.binding * string) list ->
    1.10 -    theory -> Proof.state
    1.11 -  val interpret: expression_i -> (Attrib.binding * term) list ->
    1.12 -    bool -> Proof.state -> Proof.state
    1.13 +  val interpretation: expression_i -> (Attrib.binding * term) list -> theory -> Proof.state
    1.14 +  val interpretation_cmd: expression -> (Attrib.binding * string) list -> theory -> Proof.state
    1.15 +  val interpret: expression_i -> (Attrib.binding * term) list -> bool -> Proof.state -> Proof.state
    1.16    val interpret_cmd: expression -> (Attrib.binding * string) list ->
    1.17      bool -> Proof.state -> Proof.state
    1.18