diff -r 5073cb632b6c -r 2cf86639b77e src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Tue Oct 09 15:31:45 2012 +0200
+++ b/src/Pure/Isar/proof_context.ML	Tue Oct 09 19:24:19 2012 +0200
@@ -938,8 +938,8 @@
 local
 
 fun update_thms _ (b, NONE) ctxt = ctxt |> map_facts (Facts.del (full_name ctxt b))
-  | update_thms do_props (b, SOME ths) ctxt = ctxt |> map_facts
-      (Facts.add_local (Context.Proof ctxt) do_props (b, ths) #> snd);
+  | update_thms flags (b, SOME ths) ctxt = ctxt |> map_facts
+      (Facts.add_static (Context.Proof ctxt) flags (b, ths) #> snd);
 
 in
 
@@ -952,12 +952,12 @@
     val (res, ctxt') = fold_map app facts ctxt;
     val thms = Global_Theory.name_thms false false name (flat res);
     val Mode {stmt, ...} = get_mode ctxt;
-  in ((name, thms), ctxt' |> update_thms stmt (b, SOME thms)) end);
+  in ((name, thms), ctxt' |> update_thms {strict = false, index = stmt} (b, SOME thms)) end);
 
-fun put_thms do_props thms ctxt = ctxt
+fun put_thms index thms ctxt = ctxt
   |> map_naming (K Name_Space.local_naming)
   |> Context_Position.set_visible false
-  |> update_thms do_props (apfst Binding.name thms)
+  |> update_thms {strict = false, index = index} (apfst Binding.name thms)
   |> Context_Position.restore_visible ctxt
   |> restore_naming ctxt;