# HG changeset patch # User wenzelm # Date 1726740617 -7200 # Node ID 2c75875ccf94641a33717d0c10b4f1dd53f59ad0 # Parent 51c33810397593a1ef78e45d4ec9b928c8e4763b tuned; diff -r 51c338103975 -r 2c75875ccf94 src/Pure/Syntax/printer.ML --- a/src/Pure/Syntax/printer.ML Thu Sep 19 12:08:56 2024 +0200 +++ b/src/Pure/Syntax/printer.ML Thu Sep 19 12:10:17 2024 +0200 @@ -145,12 +145,12 @@ apfst (cons (arg s_p)) (xsyms_to_syms xsyms) | xsyms_to_syms (Syntax_Ext.Space s :: xsyms) = apfst (cons (String (false, s))) (xsyms_to_syms xsyms) - | xsyms_to_syms (Syntax_Ext.Bg info :: xsyms) = + | xsyms_to_syms (Syntax_Ext.Bg block :: xsyms) = let val (bsyms, xsyms') = xsyms_to_syms xsyms; val (syms, xsyms'') = xsyms_to_syms xsyms'; in - (Block (info, bsyms) :: syms, xsyms'') + (Block (block, bsyms) :: syms, xsyms'') end | xsyms_to_syms (Syntax_Ext.Brk i :: xsyms) = apfst (cons (Break i)) (xsyms_to_syms xsyms)