diff -r de5cfda8b2de -r 5ade0b12d488 src/Pure/Isar/element.ML
--- a/src/Pure/Isar/element.ML	Tue Mar 13 11:22:39 2012 +0100
+++ b/src/Pure/Isar/element.ML	Tue Mar 13 11:23:39 2012 +0100
@@ -278,8 +278,9 @@
 
 fun gen_witness_proof proof after_qed wit_propss eq_props =
   let
-    val propss = (map o map) (fn prop => (mark_witness prop, [])) wit_propss
-      @ [map (rpair []) eq_props];
+    val propss =
+      (map o map) (fn prop => (mark_witness prop, [])) wit_propss @
+        [map (rpair []) eq_props];
     fun after_qed' thmss =
       let val (wits, eqs) = split_last ((map o map) Thm.close_derivation thmss);
       in after_qed ((map2 o map2) (curry Witness) wit_propss wits) eqs end;