tuned spaces;
authorwenzelm
Sun Feb 10 20:49:48 2008 +0100 (2008-02-10)
changeset 26054345e495d3b92
parent 26053 f8ee5cbb3068
child 26055 a7a537e0413a
tuned spaces;
src/Pure/Isar/theory_target.ML
     1.1 --- a/src/Pure/Isar/theory_target.ML	Sun Feb 10 20:49:47 2008 +0100
     1.2 +++ b/src/Pure/Isar/theory_target.ML	Sun Feb 10 20:49:48 2008 +0100
     1.3 @@ -207,7 +207,7 @@
     1.4  
     1.5  fun declare_const (ta as Target {target, is_locale, is_class, ...}) depends ((c, T), mx) lthy =
     1.6    let
     1.7 -  val pos = Position.properties_of (Position.thread_data ());
     1.8 +    val pos = Position.properties_of (Position.thread_data ());
     1.9      val xs = filter depends (#1 (ProofContext.inferred_fixes (LocalTheory.target_of lthy)));
    1.10      val U = map #2 xs ---> T;
    1.11      val (mx1, mx2, mx3) = fork_mixfix ta mx;