# HG changeset patch
# User haftmann
# Date 1447581171 -3600
# Node ID 872b2ee75359a988c79af7036a39f6a2c61af143
# Parent  0c31e1de164cece22d8b4042b837995c6069d4bb
tuned whitespace

diff -r 0c31e1de164c -r 872b2ee75359 src/Pure/Isar/interpretation.ML
--- a/src/Pure/Isar/interpretation.ML	Sun Nov 15 10:51:22 2015 +0100
+++ b/src/Pure/Isar/interpretation.ML	Sun Nov 15 10:52:51 2015 +0100
@@ -18,7 +18,7 @@
   val global_interpretation: Expression.expression_i ->
     term defines -> term rewrites -> theory -> Proof.state
   val global_sublocale: string -> Expression.expression_i ->
-    term defines -> term rewrites ->theory -> Proof.state
+    term defines -> term rewrites -> theory -> Proof.state
   val global_sublocale_cmd: xstring * Position.T -> Expression.expression ->
     string defines -> string rewrites -> theory -> Proof.state
   val sublocale: Expression.expression_i ->