# HG changeset patch
# User wenzelm
# Date 1205783483 -3600
# Node ID fb52fe23acc417a4a20452c181cd7c24644c1ecb
# Parent  73d68876ba46fb8b456df680492df3646f52f6a1
Facts.add_local;

diff -r 73d68876ba46 -r fb52fe23acc4 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Mon Mar 17 20:51:16 2008 +0100
+++ b/src/Pure/Isar/proof_context.ML	Mon Mar 17 20:51:23 2008 +0100
@@ -838,7 +838,7 @@
 
 fun update_thms _ (bname, NONE) ctxt = ctxt |> map_facts (Facts.del (full_name ctxt bname))
   | update_thms do_props (bname, SOME ths) ctxt = ctxt |> map_facts
-      (Facts.add do_props (naming_of ctxt) (full_name ctxt bname, ths));
+      (Facts.add_local do_props (naming_of ctxt) (full_name ctxt bname, ths));
 
 fun put_thms do_props thms ctxt =
   ctxt |> map_naming (K local_naming) |> update_thms do_props thms |> restore_naming ctxt;