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.
proper context;
authorwenzelm
Tue, 20 Aug 2013 20:29:38 +0200
changeset 53111 f7f1636ee2ba
parent 53106 d81211f61a1b
child 53112 04d8af9ff64b
proper context;
src/Pure/Isar/bundle.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Isar/bundle.ML	Tue Aug 20 17:39:08 2013 +0200
+++ b/src/Pure/Isar/bundle.ML	Tue Aug 20 20:29:38 2013 +0200
@@ -61,7 +61,7 @@
   let
     val (_, ctxt') = lthy |> prep_vars fixes |-> Proof_Context.add_fixes;
     val bundle0 = raw_bundle
-      |> map (fn (fact, atts) => (prep_fact lthy fact, map (prep_att lthy) atts));
+      |> map (fn (fact, atts) => (prep_fact ctxt' fact, map (prep_att ctxt') atts));
     val bundle =
       Attrib.partial_evaluation ctxt' [(Attrib.empty_binding, bundle0)] |> map snd |> flat
       |> transform_bundle (Proof_Context.export_morphism ctxt' lthy);
isabelle