src/Pure/Isar/proof_context.ML
changeset 27738 66596d7aa899
parent 27314 fce7f0c7cf76
child 27754 36df922b82d4
     1.1 --- a/src/Pure/Isar/proof_context.ML	Mon Aug 04 22:55:10 2008 +0200
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Tue Aug 05 13:31:31 2008 +0200
     1.3 @@ -859,7 +859,7 @@
     1.4            if name = "" then [Thm.transfer thy Drule.dummy_thm]
     1.5            else
     1.6              (case Facts.lookup (Context.Proof ctxt) local_facts name of
     1.7 -              SOME ths => map (Thm.transfer thy) (Facts.select thmref ths)
     1.8 +              SOME (_, ths) => map (Thm.transfer thy) (Facts.select thmref ths)
     1.9              | NONE => PureThy.get_fact (Context.Proof ctxt) thy xthmref);
    1.10        in pick name thms end;
    1.11