--- a/src/Pure/Isar/proof_context.ML Tue Feb 25 10:50:12 2014 +0100
+++ b/src/Pure/Isar/proof_context.ML Tue Feb 25 11:36:04 2014 +0100
@@ -933,7 +933,7 @@
[res] => res
| [] => err "Failed to retrieve literal fact"
| _ => err "Ambiguous specification of literal fact");
- in pick "" [res] end
+ in pick ("", Position.none) [res] end
| retrieve_thms pick ctxt xthmref =
let
val thy = theory_of ctxt;
@@ -950,7 +950,7 @@
(Name_Space.markup (Facts.space_of local_facts) name);
map (Thm.transfer thy) (Facts.select thmref ths))
| NONE => Global_Theory.get_fact (Context.Proof ctxt) thy xthmref);
- in pick name thms end;
+ in pick (name, pos) thms end;
in