prep_result: Thm.close_derivation of witness theorem avoids performance issues with proof terms;

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