# HG changeset patch
# User wenzelm
# Date 1394805583 -3600
# Node ID ed2b660a52a1b7baac07ec8606092d2fc3d88926
# Parent  8bb21318e10b184440cf8fe0266298c29b0780d7
more accurate resolution of hybrid facts, which actually changes the sort order of results;

diff -r 8bb21318e10b -r ed2b660a52a1 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Fri Mar 14 14:29:33 2014 +0100
+++ b/src/Pure/Isar/proof_context.ML	Fri Mar 14 14:59:43 2014 +0100
@@ -346,7 +346,7 @@
     val local_facts = facts_of ctxt;
     val global_facts = Global_Theory.facts_of (theory_of ctxt);
   in
-    if is_some (Facts.lookup (Context.Proof ctxt) local_facts name)
+    if Facts.defined local_facts name
     then local_facts else global_facts
   end;
 
diff -r 8bb21318e10b -r ed2b660a52a1 src/Pure/Tools/find_theorems.ML
--- a/src/Pure/Tools/find_theorems.ML	Fri Mar 14 14:29:33 2014 +0100
+++ b/src/Pure/Tools/find_theorems.ML	Fri Mar 14 14:59:43 2014 +0100
@@ -354,8 +354,9 @@
 
 fun nicer_shortest ctxt =
   let
-    val space = Facts.space_of (Proof_Context.facts_of ctxt);
-    val extern_shortest = Name_Space.extern_shortest ctxt space;
+    fun extern_shortest name =
+      Name_Space.extern_shortest ctxt
+        (Facts.space_of (Proof_Context.facts_of_fact ctxt name)) name;
 
     fun nicer (Facts.Named ((x, _), i)) (Facts.Named ((y, _), j)) =
           nicer_name (extern_shortest x, i) (extern_shortest y, j)