# HG changeset patch
# User wenzelm
# Date 1633428555 -7200
# Node ID 8e9f38240c05ecd579421f078c60e152f15b9260
# Parent  ffb15f7f26d5e55927c6d1dae599f26f0b7d7477
more exports, notably for Isabelle/Naproche;

diff -r ffb15f7f26d5 -r 8e9f38240c05 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;