# 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