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.
PureThy.get_fact: pass dynamic context;
authorwenzelm
Wed, 16 Apr 2008 17:40:41 +0200
changeset 26685 40aefd1e8f05
parent 26684 0701201def95
child 26686 9f3f5429bac6
PureThy.get_fact: pass dynamic context;
src/Pure/Isar/attrib.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Isar/attrib.ML	Wed Apr 16 17:40:40 2008 +0200
+++ b/src/Pure/Isar/attrib.ML	Wed Apr 16 17:40:41 2008 +0200
@@ -107,8 +107,8 @@
 fun attribute thy = attribute_i thy o intern_src thy;
 
 fun eval_thms ctxt args = ProofContext.note_thmss Thm.theoremK
-  [(("", []), map (apsnd (map (attribute (ProofContext.theory_of ctxt)))) args)] ctxt
-  |> (flat o map snd o fst);
+    [(("", []), map (apsnd (map (attribute (ProofContext.theory_of ctxt)))) args)] ctxt
+  |> fst |> maps snd;
 
 
 (* attributed declarations *)
@@ -162,7 +162,7 @@
 fun gen_thm pick = Scan.depend (fn context =>
   let
     val thy = Context.theory_of context;
-    val get = Context.cases PureThy.get_fact ProofContext.get_fact context;
+    val get = Context.cases (PureThy.get_fact context) ProofContext.get_fact context;
     val get_fact = get o Facts.Fact;
     val get_named = get o Facts.named;
   in
isabelle