diff -r 9e5a27486ca2 -r ce44e714d573 src/Pure/library.scala
--- a/src/Pure/library.scala	Mon Dec 26 21:28:20 2022 +0100
+++ b/src/Pure/library.scala	Tue Dec 27 11:44:37 2022 +0100
@@ -291,4 +291,7 @@
     }
     subclass(a)
   }
+
+  def as_subclass[C](c: Class[C])(x: AnyRef): Option[C] =
+    if (x == null || is_subclass(x.getClass, c)) Some(x.asInstanceOf[C]) else None
 }