--- a/src/Pure/global_theory.ML Fri Oct 18 16:25:54 2019 +0200
+++ b/src/Pure/global_theory.ML Fri Oct 18 22:44:19 2019 +0200
@@ -13,7 +13,7 @@
val alias_fact: binding -> string -> theory -> theory
val hide_fact: bool -> string -> theory -> theory
val dest_thms: bool -> theory list -> theory -> (Thm_Name.T * thm) list
- val dest_thm_names: theory -> (serial * Thm_Name.T) list
+ val dest_thm_names: theory -> (Proofterm.thm_id * Thm_Name.T) list
val lookup_thm_id: theory -> Proofterm.thm_id -> Thm_Name.T option
val lookup_thm: theory -> thm -> (Proofterm.thm_id * Thm_Name.T) option
val get_thms: theory -> xstring -> thm list
@@ -112,7 +112,12 @@
NONE => Lazy.lazy (fn () => make_thm_names thy)
| SOME lazy_tab => lazy_tab);
-val dest_thm_names = Inttab.dest o Lazy.force o get_thm_names;
+fun dest_thm_names thy =
+ let
+ val theory_name = Context.theory_long_name thy;
+ fun thm_id i = Proofterm.make_thm_id (i, theory_name);
+ val thm_names = Lazy.force (get_thm_names thy);
+ in Inttab.fold_rev (fn (i, thm_name) => cons (thm_id i, thm_name)) thm_names [] end;
fun lookup_thm_id thy =
let