1.1 --- a/src/Pure/Isar/element.ML	Tue Mar 13 11:22:39 2012 +0100
     1.2 +++ b/src/Pure/Isar/element.ML	Tue Mar 13 11:23:39 2012 +0100
     1.3 @@ -278,8 +278,9 @@
     1.4  
     1.5  fun gen_witness_proof proof after_qed wit_propss eq_props =
     1.6    let
     1.7 -    val propss = (map o map) (fn prop => (mark_witness prop, [])) wit_propss
     1.8 -      @ [map (rpair []) eq_props];
     1.9 +    val propss =
    1.10 +      (map o map) (fn prop => (mark_witness prop, [])) wit_propss @
    1.11 +        [map (rpair []) eq_props];
    1.12      fun after_qed' thmss =
    1.13        let val (wits, eqs) = split_last ((map o map) Thm.close_derivation thmss);
    1.14        in after_qed ((map2 o map2) (curry Witness) wit_propss wits) eqs end;