# HG changeset patch
# User wenzelm
# Date 1394875489 -3600
# Node ID 47015872e7950694350e8f18ffe9f8a3abe29cf6
# Parent  1b9c089ed12de257af56378edc577b27a6fb4089
clarified retrieve_generic: local error takes precedence, which is relevant for completion;

diff -r 1b9c089ed12d -r 47015872e795 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Sat Mar 15 10:14:42 2014 +0100
+++ b/src/Pure/Isar/proof_context.ML	Sat Mar 15 10:24:49 2014 +0100
@@ -917,10 +917,9 @@
 fun retrieve_global context =
   Facts.retrieve context (Global_Theory.facts_of (Context.theory_of context));
 
-fun retrieve_generic (context as Context.Proof ctxt) (xname, pos) =
-      if can (fn () => Facts.retrieve context (facts_of ctxt) (xname, Position.none)) ()
-      then Facts.retrieve context (facts_of ctxt) (xname, pos)
-      else retrieve_global context (xname, pos)
+fun retrieve_generic (context as Context.Proof ctxt) arg =
+      (Facts.retrieve context (facts_of ctxt) arg handle ERROR local_msg =>
+        (retrieve_global context arg handle ERROR _ => error local_msg))
   | retrieve_generic context arg = retrieve_global context arg;
 
 fun retrieve pick context (Facts.Fact s) =