diff --git a/org.eventb.texttools/src/org/eventb/texttools/prettyprint/MachinePrintSwitch.java b/org.eventb.texttools/src/org/eventb/texttools/prettyprint/MachinePrintSwitch.java index bf54a6043588b333117a2e11c79096bf60e87ce5..ff6b2741d4dedbc19360269ae4414b2436dcec10 100644 --- a/org.eventb.texttools/src/org/eventb/texttools/prettyprint/MachinePrintSwitch.java +++ b/org.eventb.texttools/src/org/eventb/texttools/prettyprint/MachinePrintSwitch.java @@ -251,7 +251,7 @@ public class MachinePrintSwitch extends MachineSwitch<Boolean> implements printer.appendLineBreak(); } - printer.appendWithLineBreak(VARIANT); + printer.appendWithSpace(VARIANT); printer.increaseIndentLevel(); for (final Variant variant : variants) {