equal
deleted
inserted
replaced
857 val name = Facts.name_of_ref thmref; |
857 val name = Facts.name_of_ref thmref; |
858 val thms = |
858 val thms = |
859 if name = "" then [Thm.transfer thy Drule.dummy_thm] |
859 if name = "" then [Thm.transfer thy Drule.dummy_thm] |
860 else |
860 else |
861 (case Facts.lookup (Context.Proof ctxt) local_facts name of |
861 (case Facts.lookup (Context.Proof ctxt) local_facts name of |
862 SOME ths => map (Thm.transfer thy) (Facts.select thmref ths) |
862 SOME (_, ths) => map (Thm.transfer thy) (Facts.select thmref ths) |
863 | NONE => PureThy.get_fact (Context.Proof ctxt) thy xthmref); |
863 | NONE => PureThy.get_fact (Context.Proof ctxt) thy xthmref); |
864 in pick name thms end; |
864 in pick name thms end; |
865 |
865 |
866 in |
866 in |
867 |
867 |