# HG changeset patch
# User wenzelm
# Date 1333444877 -7200
# Node ID 8f06d8ac46097ec8e601cd81391cf33b55ac1c9b
# Parent  392c4cd97e5c663415795ea1f76d64ed3383f588
tuned;

diff -r 392c4cd97e5c -r 8f06d8ac4609 src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Tue Apr 03 10:59:20 2012 +0200
+++ b/src/Pure/Isar/expression.ML	Tue Apr 03 11:21:17 2012 +0200
@@ -43,12 +43,9 @@
     (Attrib.binding * term) list -> theory -> Proof.state
   val sublocale_cmd: (local_theory -> local_theory) -> xstring * Position.T -> expression ->
     (Attrib.binding * string) list -> theory -> Proof.state
-  val interpretation: expression_i -> (Attrib.binding * term) list ->
-    theory -> Proof.state
-  val interpretation_cmd: expression -> (Attrib.binding * string) list ->
-    theory -> Proof.state
-  val interpret: expression_i -> (Attrib.binding * term) list ->
-    bool -> Proof.state -> Proof.state
+  val interpretation: expression_i -> (Attrib.binding * term) list -> theory -> Proof.state
+  val interpretation_cmd: expression -> (Attrib.binding * string) list -> theory -> Proof.state
+  val interpret: expression_i -> (Attrib.binding * term) list -> bool -> Proof.state -> Proof.state
   val interpret_cmd: expression -> (Attrib.binding * string) list ->
     bool -> Proof.state -> Proof.state