--- a/src/Pure/Isar/proof_context.ML Sun Jul 28 11:53:51 2019 +0200
+++ b/src/Pure/Isar/proof_context.ML Sun Jul 28 12:11:20 2019 +0200
@@ -1081,18 +1081,20 @@
val name = full_name ctxt b;
val ths' =
Global_Theory.check_thms_lazy ths
- |> Lazy.map_finished (Global_Theory.name_thms true false name #> map (Thm.kind_rule kind));
+ |> Lazy.map_finished
+ (Global_Theory.name_thms Global_Theory.unofficial1 name #> map (Thm.kind_rule kind));
val (_, ctxt') = add_facts {index = is_stmt ctxt} (b, ths') ctxt;
in ctxt' end;
fun note_thms kind ((b, more_atts), facts) ctxt =
let
val name = full_name ctxt b;
- val facts' = Global_Theory.burrow_fact (Global_Theory.name_thms true false name) facts;
+ val facts' = facts
+ |> Global_Theory.burrow_fact (Global_Theory.name_thms Global_Theory.unofficial1 name);
fun app (ths, atts) =
fold_map (Thm.proof_attributes (surround (Thm.kind kind) (atts @ more_atts))) ths;
val (res, ctxt') = fold_map app facts' ctxt;
- val thms = Global_Theory.name_thms false false name (flat res);
+ val thms = Global_Theory.name_thms Global_Theory.unofficial2 name (flat res);
val (_, ctxt'') = ctxt' |> add_facts {index = is_stmt ctxt} (b, Lazy.value thms);
in ((name, thms), ctxt'') end;