diff --git a/src/Lean.lean b/src/Lean.lean
index d52a3488dc..f5e62c749a 100644
--- a/src/Lean.lean
+++ b/src/Lean.lean
@@ -47,3 +47,4 @@ public import Lean.ErrorExplanation
 public import Lean.DefEqAttrib
 public import Lean.Shell
 public import Lean.ExtraModUses
+public import Lean.OriginalConstKind
diff --git a/src/Lean/AddDecl.lean b/src/Lean/AddDecl.lean
index db8f43db2a..b589f3f4c3 100644
--- a/src/Lean/AddDecl.lean
+++ b/src/Lean/AddDecl.lean
@@ -8,6 +8,8 @@ module
 prelude
 public import Lean.Meta.Sorry
 public import Lean.Util.CollectAxioms
+public import Lean.OriginalConstKind
+import all Lean.OriginalConstKind  -- for accessing `privateConstKindsExt`
 
 public section
 
@@ -45,28 +47,6 @@ where go env
   | .str p _ => if isNamespaceName p then go (env.registerNamespace p) p else env
   | _        => env
 
-private builtin_initialize privateConstKindsExt : MapDeclarationExtension ConstantKind ←
-  -- Use `sync` so we can add entries from anywhere without restrictions
-  mkMapDeclarationExtension (asyncMode := .sync)
-
-/--
-Returns the kind of the declaration as originally declared instead of as exported. This information
-is stored by `Lean.addDecl` and may be inaccurate if that function was circumvented. Returns `none`
-if the declaration was not found.
--/
-def getOriginalConstKind? (env : Environment) (declName : Name) : Option ConstantKind := do
-  -- Use `local` as for asynchronous decls from the current module, `findAsync?` below will yield
-  -- the same result but potentially earlier (after `addConstAsync` instead of `addDecl`)
-  privateConstKindsExt.find? (asyncMode := .local) env declName <|>
-    (env.setExporting false |>.findAsync? declName).map (·.kind)
-
-/--
-Checks whether the declaration was originally declared as a theorem; see also
-`Lean.getOriginalConstKind?`. Returns `false` if the declaration was not found.
--/
-def wasOriginallyTheorem (env : Environment) (declName : Name) : Bool :=
-  getOriginalConstKind? env declName |>.map (· matches .thm) |>.getD false
-
 /-- If `warn.sorry` is set to true, then, so long as the message log does not already have any errors,
 declarations with `sorryAx` generate the "declaration uses `sorry`" warning. -/
 register_builtin_option warn.sorry : Bool := {
diff --git a/src/Lean/OriginalConstKind.lean b/src/Lean/OriginalConstKind.lean
new file mode 100644
index 0000000000..16361ea893
--- /dev/null
+++ b/src/Lean/OriginalConstKind.lean
@@ -0,0 +1,43 @@
+/-
+Copyright (c) 2026 Lean FRO. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sebastian Ullrich
+-/
+module
+
+prelude
+public import Lean.Environment
+import Lean.EnvExtension
+
+namespace Lean
+
+-- No public mutating interface as this is an implementation detail of `addDecl` and separated only
+-- to avoid an import cycle.
+private builtin_initialize privateConstKindsExt : MapDeclarationExtension ConstantKind ←
+  -- Use `sync` so we can add entries from anywhere without restrictions
+  mkMapDeclarationExtension (asyncMode := .sync)
+
+/--
+Returns the kind of the declaration as originally declared instead of as exported. This information
+is stored by `Lean.addDecl` and may be inaccurate if that function was circumvented. Returns `none`
+if the declaration was not found.
+-/
+public def getOriginalConstKind? (env : Environment) (declName : Name) : Option ConstantKind := do
+  -- Use `local` as for asynchronous decls from the current module, `findAsync?` below will yield
+  -- the same result but potentially earlier (after `addConstAsync` instead of `addDecl`)
+  privateConstKindsExt.find? (asyncMode := .local) env declName <|>
+    (env.setExporting false |>.findAsync? declName).map (·.kind)
+
+/--
+Checks whether the declaration was originally declared as a definition; see also
+`Lean.getOriginalConstKind?`. Returns `false` if the declaration was not found.
+-/
+public def wasOriginallyDefn (env : Environment) (declName : Name) : Bool :=
+  getOriginalConstKind? env declName |>.map (· matches .defn) |>.getD false
+
+/--
+Checks whether the declaration was originally declared as a theorem; see also
+`Lean.getOriginalConstKind?`. Returns `false` if the declaration was not found.
+-/
+public def wasOriginallyTheorem (env : Environment) (declName : Name) : Bool :=
+  getOriginalConstKind? env declName |>.map (· matches .thm) |>.getD false
diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h
index 79a0e58edd..b3911deb05 100644
--- a/stage0/src/stdlib_flags.h
+++ b/stage0/src/stdlib_flags.h
@@ -1,5 +1,7 @@
 #include "util/options.h"
 
+// Dear CI, please update stage 0
+
 namespace lean {
 options get_default_options() {
     options opts;