src/Pure/Isar/proof_context.ML
changeset 26309 fb52fe23acc4
parent 26284 533dcb120a8e
child 26321 d875e70a94de
     1.1 --- a/src/Pure/Isar/proof_context.ML	Mon Mar 17 20:51:16 2008 +0100
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Mon Mar 17 20:51:23 2008 +0100
     1.3 @@ -838,7 +838,7 @@
     1.4  
     1.5  fun update_thms _ (bname, NONE) ctxt = ctxt |> map_facts (Facts.del (full_name ctxt bname))
     1.6    | update_thms do_props (bname, SOME ths) ctxt = ctxt |> map_facts
     1.7 -      (Facts.add do_props (naming_of ctxt) (full_name ctxt bname, ths));
     1.8 +      (Facts.add_local do_props (naming_of ctxt) (full_name ctxt bname, ths));
     1.9  
    1.10  fun put_thms do_props thms ctxt =
    1.11    ctxt |> map_naming (K local_naming) |> update_thms do_props thms |> restore_naming ctxt;