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.
always register proofs, even for empty binding;
authorwenzelm
Fri, 31 Aug 2012 22:25:06 +0200
changeset 49059 be6d4e8307c8
parent 49058 2924a83a4a0b
child 49060 fa094e173cb9
always register proofs, even for empty binding;
src/Pure/Isar/specification.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Isar/specification.ML	Fri Aug 31 22:24:14 2012 +0200
+++ b/src/Pure/Isar/specification.ML	Fri Aug 31 22:25:06 2012 +0200
@@ -395,7 +395,8 @@
       let
         val results' = burrow (map Goal.norm_result o Proof_Context.export goal_ctxt' lthy) results;
         val (res, lthy') =
-          if forall (Attrib.is_empty_binding o fst) stmt then (map (pair "") results', lthy)
+          if forall (Attrib.is_empty_binding o fst) stmt
+          then (map (pair "") results', Local_Theory.register_proofs (flat results) lthy)
           else
             Local_Theory.notes_kind kind
               (map2 (fn (b, _) => fn ths => (b, [(ths, [])])) stmt results') lthy;
isabelle