# HG changeset patch
# User wenzelm
# Date 1208555384 -7200
# Node ID 0696461110885f65fadd1b9e389e1387254e4b44
# Parent  8d1925ad0dac27d44013fc1dd779148d5c6d18ca
tuned;

diff -r 8d1925ad0dac -r 069646111088 src/Pure/Isar/element.ML
--- a/src/Pure/Isar/element.ML	Fri Apr 18 23:49:40 2008 +0200
+++ b/src/Pure/Isar/element.ML	Fri Apr 18 23:49:44 2008 +0200
@@ -174,7 +174,7 @@
 
     fun prt_var (x, SOME T) = Pretty.block [Pretty.str (x ^ " ::"), Pretty.brk 1, prt_typ T]
       | prt_var (x, NONE) = Pretty.str x;
-    val prt_vars =  separate (Pretty.keyword "and") o map prt_var;
+    val prt_vars = separate (Pretty.keyword "and") o map prt_var;
 
     fun prt_obtain (_, ([], ts)) = Pretty.block (Pretty.breaks (prt_terms ts))
       | prt_obtain (_, (xs, ts)) = Pretty.block (Pretty.breaks