--- 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;