--- a/src/Pure/Syntax/syntax_phases.ML Tue Oct 15 14:39:54 2024 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML Tue Oct 15 14:55:45 2024 +0200
@@ -658,7 +658,7 @@
in
-fun term_to_ast ctxt trf term =
+fun term_to_ast ctxt trf =
let
val show_types = Config.get ctxt show_types orelse Config.get ctxt show_sorts;
val show_markup = Config.get ctxt show_markup;
@@ -668,45 +668,44 @@
val show_var_types = show_types orelse show_markup;
val clean_var_types = show_markup andalso not show_types;
- fun constrain_ast clean T ast =
+ fun constrain clean T ast =
let val U = Type_Annotation.print clean T
in Ast.Appl [Ast.Constant "_constrain", ast, ast_of_termT ctxt trf (term_of_typ ctxt U)] end;
- fun ast_of tm =
+ fun main tm =
(case strip_comb tm of
- (t as Abs _, ts) => Ast.mk_appl (ast_of (Syntax_Trans.abs_tr' ctxt t)) (map ast_of ts)
+ (t as Abs _, ts) => Ast.mk_appl (main (Syntax_Trans.abs_tr' ctxt t)) (map main ts)
| ((c as Const ("_free", _)), Free (x, T) :: ts) =>
- Ast.mk_appl (var_ast (c $ Syntax.free x) T) (map ast_of ts)
+ Ast.mk_appl (variable (c $ Syntax.free x) T) (map main ts)
| ((c as Const ("_var", _)), Var (xi, T) :: ts) =>
- Ast.mk_appl (var_ast (c $ Syntax.var xi) T) (map ast_of ts)
+ Ast.mk_appl (variable (c $ Syntax.var xi) T) (map main ts)
| ((c as Const ("_bound", B)), Free (x, T) :: ts) =>
let
val X =
if show_markup andalso not show_types orelse B <> dummyT then T
else dummyT;
- in Ast.mk_appl (var_ast (c $ Syntax.free x) X) (map ast_of ts) end
+ in Ast.mk_appl (variable (c $ Syntax.free x) X) (map main ts) end
| (Const ("_idtdummy", T), ts) =>
- Ast.mk_appl (var_ast (Syntax.const "_idtdummy") T) (map ast_of ts)
- | (Const (c, T), ts) => const_ast c T ts
- | (t, ts) => Ast.mk_appl (simple_ast_of ctxt t) (map ast_of ts))
+ Ast.mk_appl (variable (Syntax.const "_idtdummy") T) (map main ts)
+ | (Const (c, T), ts) => constant c T ts
+ | (t, ts) => Ast.mk_appl (simple_ast_of ctxt t) (map main ts))
- and const_ast a T args =
+ and constant a T args =
(case SOME (trf a ctxt (Type_Annotation.smash T) args) handle Match => NONE of
- SOME t => ast_of t
+ SOME t => main t
| NONE =>
- let val c = Ast.Constant a |> show_const_types ? constrain_ast {clean = true} T
- in Ast.mk_appl c (map ast_of args) end)
+ let val c = Ast.Constant a |> show_const_types ? constrain {clean = true} T
+ in Ast.mk_appl c (map main args) end)
- and var_ast v T =
+ and variable v T =
simple_ast_of ctxt v
- |> show_var_types ? constrain_ast {clean = clean_var_types} T;
+ |> show_var_types ? constrain {clean = clean_var_types} T;
in
- term
- |> mark_aprop
- |> show_types ? prune_types
- |> Variable.revert_bounds ctxt
- |> mark_atoms ctxt
- |> ast_of
+ mark_aprop
+ #> show_types ? prune_types
+ #> Variable.revert_bounds ctxt
+ #> mark_atoms ctxt
+ #> main
end;
end;