--- a/src/Pure/Isar/generic_target.ML Sun Jul 28 11:53:51 2019 +0200
+++ b/src/Pure/Isar/generic_target.ML Sun Jul 28 12:11:20 2019 +0200
@@ -277,7 +277,7 @@
|> Drule.zero_var_indexes_list;
(*thm definition*)
- val result = Global_Theory.name_thm true true name th'';
+ val result = Global_Theory.name_thm Global_Theory.official1 name th'';
(*import fixes*)
val (tvars, vars) =
@@ -299,7 +299,7 @@
handle THM _ => raise THM ("Failed to re-import result", 0, result' :: asms'))
|> Local_Defs.contract ctxt defs (Thm.cprop_of th)
|> Goal.norm_result ctxt
- |> Global_Theory.name_thm false false name;
+ |> Global_Theory.name_thm Global_Theory.unofficial2 name;
in (result'', result) end;
--- 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;
--- a/src/Pure/global_theory.ML Sun Jul 28 11:53:51 2019 +0200
+++ b/src/Pure/global_theory.ML Sun Jul 28 12:11:20 2019 +0200
@@ -21,8 +21,13 @@
val burrow_facts: ('a list -> 'b list) ->
('c * ('a list * 'd) list) list -> ('c * ('b list * 'd) list) list
val name_multi: string -> 'a list -> (string * 'a) list
- val name_thm: bool -> bool -> string -> thm -> thm
- val name_thms: bool -> bool -> string -> thm list -> thm list
+ type name_flags = {pre: bool, official: bool}
+ val official1: name_flags
+ val official2: name_flags
+ val unofficial1: name_flags
+ val unofficial2: name_flags
+ val name_thm: name_flags -> string -> thm -> thm
+ val name_thms: name_flags -> string -> thm list -> thm list
val check_thms_lazy: thm list lazy -> thm list lazy
val add_thms_lazy: string -> (binding * thm list lazy) -> theory -> theory
val store_thm: binding * thm -> theory -> thm * theory
@@ -107,18 +112,26 @@
(* naming *)
-fun name_multi name [x] = [(name, x)]
- | name_multi "" xs = map (pair "") xs
- | name_multi name xs = map_index (fn (i, x) => (name ^ "_" ^ string_of_int (i + 1), x)) xs;
+type name_flags = {pre: bool, official: bool};
-fun name_thm pre official name thm = thm
+val official1 : name_flags = {pre = true, official = true};
+val official2 : name_flags = {pre = false, official = true};
+val unofficial1 : name_flags = {pre = true, official = false};
+val unofficial2 : name_flags = {pre = false, official = false};
+
+fun name_thm {pre, official} name thm = thm
|> (official andalso not (pre andalso Thm.derivation_name thm <> "")) ?
Thm.name_derivation name
|> (name <> "" andalso not (pre andalso Thm.has_name_hint thm)) ?
Thm.put_name_hint name;
-fun name_thms pre official name thms =
- map (uncurry (name_thm pre official)) (name_multi name thms);
+
+fun name_multi name [x] = [(name, x)]
+ | name_multi "" xs = map (pair "") xs
+ | name_multi name xs = map_index (fn (i, x) => (name ^ "_" ^ string_of_int (i + 1), x)) xs;
+
+fun name_thms name_flags name thms =
+ map (uncurry (name_thm name_flags)) (name_multi name thms);
(* apply theorems and attributes *)
@@ -164,7 +177,7 @@
val name = Sign.full_name thy b;
val thms' =
check_thms_lazy thms
- |> Lazy.map_finished (name_thms true true name #> map (Thm.kind_rule kind));
+ |> Lazy.map_finished (name_thms official1 name #> map (Thm.kind_rule kind));
in thy |> Thm.register_proofs thms' |> add_facts (b, thms') end;
val app_facts =
@@ -185,16 +198,16 @@
(* store_thm *)
fun store_thm (b, th) =
- apply_facts (name_thms true true) (name_thms false true) (b, [([th], [])]) #>> the_single;
+ apply_facts (name_thms official1) (name_thms official2) (b, [([th], [])]) #>> the_single;
fun store_thm_open (b, th) =
- apply_facts (name_thms true false) (name_thms false false) (b, [([th], [])]) #>> the_single;
+ apply_facts (name_thms unofficial1) (name_thms unofficial2) (b, [([th], [])]) #>> the_single;
(* add_thms(s) *)
fun add_thms_atts pre_name ((b, thms), atts) =
- apply_facts pre_name (name_thms false true) (b, [(thms, atts)]);
+ apply_facts pre_name (name_thms official2) (b, [(thms, atts)]);
fun gen_add_thmss pre_name =
fold_map (add_thms_atts pre_name);
@@ -202,8 +215,8 @@
fun gen_add_thms pre_name args =
apfst (map hd) o gen_add_thmss pre_name (map (apfst (apsnd single)) args);
-val add_thmss = gen_add_thmss (name_thms true true);
-val add_thms = gen_add_thms (name_thms true true);
+val add_thmss = gen_add_thmss (name_thms official1);
+val add_thms = gen_add_thms (name_thms official1);
val add_thm = yield_singleton add_thms;
@@ -223,7 +236,7 @@
let
val name = Sign.full_name thy b;
val facts' = facts |> map (apsnd (fn atts => surround (Thm.kind kind) (atts @ more_atts)));
- val (thms', thy') = thy |> apply_facts (name_thms true true) (name_thms false true) (b, facts');
+ val (thms', thy') = thy |> apply_facts (name_thms official1) (name_thms official2) (b, facts');
in ((name, thms'), thy') end;
val note_thmss = fold_map o note_thms;