src/Pure/Isar/proof_context.ML
changeset 26393 42febbed5460
parent 26361 7946f459c6c8
child 26435 bdce320cd426
     1.1 --- a/src/Pure/Isar/proof_context.ML	Tue Mar 25 19:39:58 2008 +0100
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Tue Mar 25 19:39:59 2008 +0100
     1.3 @@ -811,7 +811,7 @@
     1.4          val thms =
     1.5            if name = "" then [Thm.transfer thy Drule.dummy_thm]
     1.6            else
     1.7 -            (case Facts.lookup local_facts name of
     1.8 +            (case Facts.lookup (Context.Proof ctxt) local_facts name of
     1.9                SOME ths => map (Thm.transfer thy) (Facts.select thmref ths)
    1.10              | NONE => from_thy thy xthmref);
    1.11        in pick name thms end;