# HG changeset patch # User wenzelm # Date 1724437264 -7200 # Node ID 232a839ef8e6536d71a402251ff5b11481808acf # Parent 43c4817375bf0d4346d9d119ec9d5e47ffd6f976 clarified signature: more operations; diff -r 43c4817375bf -r 232a839ef8e6 src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Fri Aug 23 18:38:44 2024 +0200 +++ b/src/Pure/Isar/proof_context.ML Fri Aug 23 20:21:04 2024 +0200 @@ -155,6 +155,7 @@ val apply_case: Rule_Cases.T -> Proof.context -> (string * term list) list * Proof.context val check_case: Proof.context -> bool -> string * Position.T -> binding option list -> Rule_Cases.T + val is_syntax_const: Proof.context -> string -> bool val check_syntax_const: Proof.context -> string * Position.T -> string val syntax: bool -> Syntax.mode -> (string * typ * mixfix) list -> Proof.context -> Proof.context @@ -1125,8 +1126,10 @@ (* syntax *) +val is_syntax_const = Syntax.is_const o syntax_of; + fun check_syntax_const ctxt (c, pos) = - if Syntax.is_const (syntax_of ctxt) c then c + if is_syntax_const ctxt c then c else error ("Unknown syntax const: " ^ quote c ^ Position.here pos); fun syntax add mode args ctxt = diff -r 43c4817375bf -r 232a839ef8e6 src/Pure/Syntax/syntax_phases.ML --- a/src/Pure/Syntax/syntax_phases.ML Fri Aug 23 18:38:44 2024 +0200 +++ b/src/Pure/Syntax/syntax_phases.ML Fri Aug 23 20:21:04 2024 +0200 @@ -620,7 +620,7 @@ in (t1' $ t2', seen'') end; in #1 (prune (tm, [])) end; -fun mark_atoms is_syntax_const ctxt tm = +fun mark_atoms ctxt tm = let val {structs, fixes} = Syntax_Trans.get_idents ctxt; val show_structs = Config.get ctxt show_structs; @@ -631,7 +631,7 @@ | mark (t $ u) = mark t $ mark u | mark (Abs (x, T, t)) = Abs (x, T, mark t) | mark (t as Const (c, T)) = - if is_syntax_const c then t + if Proof_Context.is_syntax_const ctxt c then t else Const (Lexicon.mark_const c, T) | mark (t as Free (x, T)) = let val i = find_index (fn s => s = x) structs + 1 in @@ -651,8 +651,6 @@ fun term_to_ast ctxt trf tm = let - val is_syntax_const = Syntax.is_const (Proof_Context.syntax_of ctxt); - val show_types = Config.get ctxt show_types orelse Config.get ctxt show_sorts; val show_markup = Config.get ctxt show_markup; @@ -694,7 +692,7 @@ |> mark_aprop |> show_types ? prune_types |> Variable.revert_bounds ctxt - |> mark_atoms is_syntax_const ctxt + |> mark_atoms ctxt |> ast_of end;