more accurate resolution of hybrid facts, which actually changes the sort order of results;
1.1 --- a/src/Pure/Isar/proof_context.ML Fri Mar 14 14:29:33 2014 +0100
1.2 +++ b/src/Pure/Isar/proof_context.ML Fri Mar 14 14:59:43 2014 +0100
1.3 @@ -346,7 +346,7 @@
1.4 val local_facts = facts_of ctxt;
1.5 val global_facts = Global_Theory.facts_of (theory_of ctxt);
1.6 in
1.7 - if is_some (Facts.lookup (Context.Proof ctxt) local_facts name)
1.8 + if Facts.defined local_facts name
1.9 then local_facts else global_facts
1.10 end;
1.11
2.1 --- a/src/Pure/Tools/find_theorems.ML Fri Mar 14 14:29:33 2014 +0100
2.2 +++ b/src/Pure/Tools/find_theorems.ML Fri Mar 14 14:59:43 2014 +0100
2.3 @@ -354,8 +354,9 @@
2.4
2.5 fun nicer_shortest ctxt =
2.6 let
2.7 - val space = Facts.space_of (Proof_Context.facts_of ctxt);
2.8 - val extern_shortest = Name_Space.extern_shortest ctxt space;
2.9 + fun extern_shortest name =
2.10 + Name_Space.extern_shortest ctxt
2.11 + (Facts.space_of (Proof_Context.facts_of_fact ctxt name)) name;
2.12
2.13 fun nicer (Facts.Named ((x, _), i)) (Facts.Named ((y, _), j)) =
2.14 nicer_name (extern_shortest x, i) (extern_shortest y, j)