Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/thm.ML
changeset 80295 8a9588ffc133
parent 80289 40a6a6ac1669 
--- a/src/Pure/thm.ML	Fri Jun 07 15:20:01 2024 +0200
+++ b/src/Pure/thm.ML	Fri Jun 07 23:53:31 2024 +0200
@@ -118,11 +118,11 @@
   val extra_shyps: thm -> sort list
   val strip_shyps: thm -> thm
   val derivation_closed: thm -> bool
-  val derivation_name: thm -> string
+  val derivation_name: thm -> Thm_Name.T
   val derivation_id: thm -> Proofterm.thm_id option
-  val raw_derivation_name: thm -> string
-  val expand_name: thm -> Proofterm.thm_header -> string option
-  val name_derivation: string * Position.T -> thm -> thm
+  val raw_derivation_name: thm -> Thm_Name.T
+  val expand_name: thm -> Proofterm.thm_header -> Thm_Name.T option
+  val name_derivation: Thm_Name.P -> thm -> thm
   val close_derivation: Position.T -> thm -> thm
   val trim_context: thm -> thm
   val axiom: theory -> string -> thm
@@ -1130,7 +1130,9 @@
       (case Proofterm.get_identity shyps hyps prop (Proofterm.proof_of body) of
         NONE => K false
       | SOME {serial, ...} => fn (header: Proofterm.thm_header) => serial = #serial header);
-    fun expand header = if self_id header orelse #name header = "" then SOME "" else NONE;
+    fun expand header =
+      if self_id header orelse Thm_Name.is_empty (#thm_name header)
+      then SOME Thm_Name.empty else NONE;
   in expand end;
 
 (*deterministic name of finished proof*)
@@ -1166,7 +1168,7 @@
 fun close_derivation pos =
   solve_constraints #> (fn thm =>
     if not (null (tpairs_of thm)) orelse derivation_closed thm then thm
-    else name_derivation ("", pos) thm);
+    else name_derivation (Thm_Name.empty, pos) thm);
 
 val trim_context = solve_constraints #> trim_context_thm;
isabelle