--- a/src/Pure/context.ML Thu Mar 30 16:09:19 2023 +0200
+++ b/src/Pure/context.ML Thu Mar 30 16:10:50 2023 +0200
@@ -55,7 +55,7 @@
val join_thys: theory * theory -> theory
val begin_thy: string -> theory list -> theory
val finish_thy: theory -> theory
- val theory_sizeof1_data: theory -> (Position.T * int) list
+ val theory_data_sizeof1: theory -> (Position.T * int) list
(*proof context*)
val raw_transfer: theory -> Proof.context -> Proof.context
(*certificate*)
@@ -460,7 +460,7 @@
end;
-fun theory_sizeof1_data thy =
+fun theory_data_sizeof1 thy =
build (data_of thy |> Datatab.fold_rev (fn (k, _) =>
(case Theory_Data.sizeof1 k thy of
NONE => I