Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/Isar/proof_context.ML
changeset 27738 66596d7aa899
parent 27314 fce7f0c7cf76
child 27754 36df922b82d4 
--- a/src/Pure/Isar/proof_context.ML	Mon Aug 04 22:55:10 2008 +0200
+++ b/src/Pure/Isar/proof_context.ML	Tue Aug 05 13:31:31 2008 +0200
@@ -859,7 +859,7 @@
           if name = "" then [Thm.transfer thy Drule.dummy_thm]
           else
             (case Facts.lookup (Context.Proof ctxt) local_facts name of
-              SOME ths => map (Thm.transfer thy) (Facts.select thmref ths)
+              SOME (_, ths) => map (Thm.transfer thy) (Facts.select thmref ths)
             | NONE => PureThy.get_fact (Context.Proof ctxt) thy xthmref);
       in pick name thms end;
isabelle