diff -r 3d9ea64f2c39 -r e6cd6dd07d7a src/Tools/isac/ProgLang/ListC.thy
--- a/src/Tools/isac/ProgLang/ListC.thy	Wed Dec 02 12:32:30 2020 +0100
+++ b/src/Tools/isac/ProgLang/ListC.thy	Mon Dec 07 17:39:21 2020 +0100
@@ -60,10 +60,10 @@
 xfoldr_Nil:  "xfoldr f {|| ||} = id" |
 xfoldr_Cons: "xfoldr f (x @# xs) = f x \<circ> xfoldr f xs"
 
-primrec LENGTH   :: "'a list => real"
+primrec Length   :: "'a list => real"
 where
-LENGTH_NIL:	"LENGTH [] = 0" |
-LENGTH_CONS: "LENGTH (x#xs) = 1 + LENGTH xs"
+LENGTH_NIL:	"Length [] = 0" |
+LENGTH_CONS: "Length (x#xs) = 1 + Length xs"
 
 subsection \<open>Functions for 'list'\<close>