# HG changeset patch
# User wenzelm
# Date 1202672988 -3600
# Node ID 345e495d3b92557e3ddf021754870a6ce93700d7
# Parent  f8ee5cbb3068f919bcdd2643c3f35f6575d40b9a
tuned spaces;

diff -r f8ee5cbb3068 -r 345e495d3b92 src/Pure/Isar/theory_target.ML
--- a/src/Pure/Isar/theory_target.ML	Sun Feb 10 20:49:47 2008 +0100
+++ b/src/Pure/Isar/theory_target.ML	Sun Feb 10 20:49:48 2008 +0100
@@ -207,7 +207,7 @@
 
 fun declare_const (ta as Target {target, is_locale, is_class, ...}) depends ((c, T), mx) lthy =
   let
-  val pos = Position.properties_of (Position.thread_data ());
+    val pos = Position.properties_of (Position.thread_data ());
     val xs = filter depends (#1 (ProofContext.inferred_fixes (LocalTheory.target_of lthy)));
     val U = map #2 xs ---> T;
     val (mx1, mx2, mx3) = fork_mixfix ta mx;