# HG changeset patch
# User wenzelm
# Date 1230660462 -3600
# Node ID ef3e2c3399d7bb40ddd4c7350871de854bbfd11e
# Parent  ea97aa6aeba2b790c69d6a3b1ba1e6913a3519ca
prep_result: Thm.close_derivation of witness theorem avoids performance issues with proof terms;

diff -r ea97aa6aeba2 -r ef3e2c3399d7 src/Pure/Isar/expression.ML
--- 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 **)