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)))