# HG changeset patch
# User Andreas Lochbihler
# Date 1421245370 -3600
# Node ID 07b9893cd8a7cb126aa89995ec738fda87bfadf2
# Parent  7fd531cc0172b04f25eaf3c740b6764e055ab5ee
indent broken lines of bindings in do blocks

diff -r 7fd531cc0172 -r 07b9893cd8a7 src/HOL/Library/Monad_Syntax.thy
--- a/src/HOL/Library/Monad_Syntax.thy	Wed Jan 14 13:51:34 2015 +0100
+++ b/src/HOL/Library/Monad_Syntax.thy	Wed Jan 14 15:22:50 2015 +0100
@@ -41,7 +41,7 @@
 
 syntax
   "_do_block" :: "do_binds \<Rightarrow> 'a" ("do {//(2  _)//}" [12] 62)
-  "_do_bind" :: "[pttrn, 'a] \<Rightarrow> do_bind" ("(_ <-/ _)" 13)
+  "_do_bind" :: "[pttrn, 'a] \<Rightarrow> do_bind" ("(2_ <-/ _)" 13)
   "_do_let" :: "[pttrn, 'a] \<Rightarrow> do_bind" ("(2let _ =/ _)" [1000, 13] 13)
   "_do_then" :: "'a \<Rightarrow> do_bind" ("_" [14] 13)
   "_do_final" :: "'a \<Rightarrow> do_binds" ("_")
@@ -49,7 +49,7 @@
   "_thenM" :: "['a, 'b] \<Rightarrow> 'c" (infixr ">>" 54)
 
 syntax (xsymbols)
-  "_do_bind"  :: "[pttrn, 'a] \<Rightarrow> do_bind" ("(_ \<leftarrow>/ _)" 13)
+  "_do_bind"  :: "[pttrn, 'a] \<Rightarrow> do_bind" ("(2_ \<leftarrow>/ _)" 13)
   "_thenM" :: "['a, 'b] \<Rightarrow> 'c" (infixr "\<guillemotright>" 54)
 
 syntax (latex output)