src/HOL/Imperative_HOL/ex/Linked_Lists.thy

 fun make_llist :: "'a\<Colon>heap list \<Rightarrow> 'a node Heap"
 where 
   [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 *}
 
 definition