more exports, notably for Isabelle/Naproche;
authorwenzelm
Tue, 05 Oct 2021 12:09:15 +0200
changeset 74461 8e9f38240c05
parent 74460 ffb15f7f26d5
child 74462 b3d6bb2ebf77
more exports, notably for Isabelle/Naproche;
src/Pure/context.ML
--- a/src/Pure/context.ML	Tue Oct 05 00:04:01 2021 +0200
+++ b/src/Pure/context.ML	Tue Oct 05 12:09:15 2021 +0200
@@ -39,6 +39,7 @@
   val theory_long_name: theory -> string
   val theory_name: theory -> string
   val theory_name': {long: bool} -> theory -> string
+  val theory_identifier: theory -> serial
   val PureN: string
   val pretty_thy: theory -> Pretty.T
   val pretty_abbrev_thy: theory -> Pretty.T
@@ -155,7 +156,6 @@
 
 val theory_identity = #1 o rep_theory;
 val theory_id = #theory_id o theory_identity;
-
 val identity_of_id = #1 o rep_theory_id;
 val identity_of = identity_of_id o theory_id;
 val history_of_id = #2 o rep_theory_id;
@@ -173,6 +173,7 @@
 val theory_long_name = #name o history_of;
 val theory_name = Long_Name.base_name o theory_long_name;
 fun theory_name' {long} = if long then theory_long_name else theory_name;
+val theory_identifier = #id o identity_of_id o theory_id;
 
 val parents_of = #parents o ancestry_of;
 val ancestors_of = #ancestors o ancestry_of;