# HG changeset patch
# User wenzelm
# Date 1564308680 -7200
# Node ID 973bf3e42e54e72f0d8e954e7ac95ef61e9d862b
# Parent  198be2de1efaaf7645cfb2ba60e59f966c6b92e9
clarified signature;

diff -r 198be2de1efa -r 973bf3e42e54 src/Pure/Isar/generic_target.ML
--- 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;
 
diff -r 198be2de1efa -r 973bf3e42e54 src/Pure/Isar/proof_context.ML
--- 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;
 
diff -r 198be2de1efa -r 973bf3e42e54 src/Pure/global_theory.ML
--- 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;