# HG changeset patch
# User haftmann
# Date 1280399325 -7200
# Node ID 7775fdc52b6dde1e15b1f1245096c498d33f7f46
# Parent  00042fd999a80838a453cab389dbd4a51fd8bc04
tuned example

diff -r 00042fd999a8 -r 7775fdc52b6d src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy
--- a/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy	Thu Jul 29 12:28:45 2010 +0200
+++ b/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy	Thu Jul 29 12:28:45 2010 +0200
@@ -110,7 +110,7 @@
       subarray_def sublist'_all rev.simps[where j=0] elim!: crel_elims)
   (drule sym[of "List.length (Array.get h a)"], simp)
 
-definition "example = (Array.of_list [1::nat, 2, 3, 4, 5, 6, 7, 8, 9, 10] \<guillemotright>= (\<lambda>a. rev a 0 9))"
+definition "example = (Array.make 10 id \<guillemotright>= (\<lambda>a. rev a 0 9))"
 
 export_code example checking SML SML_imp OCaml? OCaml_imp? Haskell? Scala? Scala_imp?