--- a/thys/Abacus_Defs.thy	Fri Dec 21 12:31:36 2018 +0100
+++ b/thys/Abacus_Defs.thy	Fri Dec 21 15:30:24 2018 +0100
@@ -2,7 +2,7 @@
    Author: Jian Xu, Xingyuan Zhang, and Christian Urban
 *)
 
-header {* Alternative Definitions for Translating Abacus Machines to TMs *}
+chapter {* Alternative Definitions for Translating Abacus Machines to TMs *}
 
 theory Abacus_Defs
 imports Abacus
@@ -13,7 +13,7 @@
 
 fun address :: "abc_prog \<Rightarrow> nat \<Rightarrow> nat"
   where
-  "address p x = (Suc (listsum (take x (layout p)))) "
+  "address p x = (Suc (sum_list (take x (layout p)))) "
 
 abbreviation
   "TMGoto \<equiv> [(Nop, 1), (Nop, 1)]"