src/Pure/Isar/isar_cmd.ML
changeset 80632 3a196e63a80d
parent 78797 fc598652fb8a
child 80750 1319c729c65d
--- a/src/Pure/Isar/isar_cmd.ML	Sat Aug 03 13:12:58 2024 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Sun Aug 04 12:21:13 2024 +0200
@@ -98,7 +98,7 @@
   let
     val ctxt = Proof_Context.init_global thy;
     val read_root =
-      #1 o dest_Type o Proof_Context.read_type_name {proper = true, strict = false} ctxt;
+      dest_Type_name o Proof_Context.read_type_name {proper = true, strict = false} ctxt;
   in
     raw_rules
     |> map (Syntax.map_trrule (fn (r, s) => Syntax_Phases.parse_ast_pattern ctxt (read_root r, s)))