1.1 --- a/src/Pure/Isar/expression.ML	Tue Dec 30 11:10:01 2008 +0100
     1.2 +++ b/src/Pure/Isar/expression.ML	Tue Dec 30 19:07:42 2008 +0100
     1.3 @@ -758,8 +758,8 @@
     1.4  
     1.5  fun prep_propp propss = propss |> map (map (rpair [] o Element.mark_witness));
     1.6  
     1.7 -fun prep_result propps thmss =
     1.8 -  ListPair.map (fn (props, thms) => map2 Element.make_witness props thms) (propps, thmss);
     1.9 +val prep_result = map2 (fn props => fn thms =>
    1.10 +  map2 Element.make_witness props (map Thm.close_derivation thms));
    1.11  
    1.12  
    1.13  (** Interpretation between locales: declaring sublocale relationships **)