# HG changeset patch
# User haftmann
# Date 1531939881 -7200
# Node ID 16cc1161ad7f73a142766fc9281cdbd5195ab2fb
# Parent  65ad2bfc19d284ab5cf229fdc5f70ce44991dab5
tuned equation

diff -r 65ad2bfc19d2 -r 16cc1161ad7f src/HOL/Library/IArray.thy
--- a/src/HOL/Library/IArray.thy	Wed Jul 18 20:51:20 2018 +0200
+++ b/src/HOL/Library/IArray.thy	Wed Jul 18 20:51:21 2018 +0200
@@ -52,7 +52,7 @@
 subsection \<open>Generic code equations\<close>
 
 lemma [code]:
-  "size (as :: 'a iarray) = Suc (length (IArray.list_of as))"
+  "size (as :: 'a iarray) = Suc (IArray.length as)"
   by (cases as) simp
 
 lemma [code]: