src/HOL/Imperative_HOL/ex/Linked_Lists.thy

--- a/src/HOL/Imperative_HOL/ex/Linked_Lists.thy	Mon Mar 01 17:45:19 2010 +0100
+++ b/src/HOL/Imperative_HOL/ex/Linked_Lists.thy	Mon Mar 01 21:41:35 2010 +0100
@@ -27,8 +27,8 @@
   [simp del]: "make_llist []     = return Empty"
             | "make_llist (x#xs) = do tl   \<leftarrow> make_llist xs;
                                       next \<leftarrow> Ref.new tl;
-	                              return (Node x next)
-		                   done"
+                                      return (Node x next)
+                                   done"
 
 
 text {* define traverse using the MREC combinator *}