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.
tuned;
authorwenzelm
Tue, 16 May 2023 19:42:19 +0200
changeset 78066 e6343330e8df
parent 78065 11d6a1e62841
child 78067 a71bfc551891
tuned;
src/Pure/Isar/bundle.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Isar/bundle.ML	Tue May 16 19:20:18 2023 +0200
+++ b/src/Pure/Isar/bundle.ML	Tue May 16 19:42:19 2023 +0200
@@ -124,7 +124,8 @@
     val bundle0 = raw_bundle
       |> map (fn (fact, atts) => (prep_fact ctxt' fact, map (prep_att ctxt') atts));
     val bundle =
-      Attrib.partial_evaluation ctxt' [(Binding.empty_atts, bundle0)] |> map snd |> flat
+      Attrib.partial_evaluation ctxt' [(Binding.empty_atts, bundle0)]
+      |> maps #2
       |> transform_bundle (Proof_Context.export_morphism ctxt' lthy);
   in
     lthy |> Local_Theory.declaration {syntax = false, pervasive = true}
isabelle