equal
deleted
inserted
replaced
622 else if i = 1 andalso not show_structs then |
622 else if i = 1 andalso not show_structs then |
623 Syntax.const "_struct" $ Syntax.const "_indexdefault" |
623 Syntax.const "_struct" $ Syntax.const "_indexdefault" |
624 else Syntax.const "_free" $ t |
624 else Syntax.const "_free" $ t |
625 end |
625 end |
626 | mark (t as Var (xi, T)) = |
626 | mark (t as Var (xi, T)) = |
627 if xi = Syntax_Ext.dddot_indexname then Const ("_DDDOT", T) |
627 if xi = Auto_Bind.dddot then Const ("_DDDOT", T) |
628 else Syntax.const "_var" $ t |
628 else Syntax.const "_var" $ t |
629 | mark a = a; |
629 | mark a = a; |
630 in mark tm end; |
630 in mark tm end; |
631 |
631 |
632 in |
632 in |