--- 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 =
--- 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;