Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
merged
authorwenzelm
Tue, 30 Dec 2008 19:08:43 +0100
changeset 29255 477635dc8f0e
parent 29253 3c6cd80a4854 (current diff)
parent 29254 ef3e2c3399d7 (diff)
child 29256 2f1759641087
merged
--- a/src/Pure/Isar/expression.ML	Tue Dec 30 16:50:46 2008 +0100
+++ b/src/Pure/Isar/expression.ML	Tue Dec 30 19:08:43 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 **)
isabelle