diff -r 7a91490c1b04 -r 6356d2523f73 src/HOL/MicroJava/BV/LBVComplete.thy
--- a/src/HOL/MicroJava/BV/LBVComplete.thy	Mon Dec 20 18:25:22 2004 +0100
+++ b/src/HOL/MicroJava/BV/LBVComplete.thy	Wed Dec 22 11:36:33 2004 +0100
@@ -15,7 +15,7 @@
 
   make_cert :: "['s step_type, 's list, 's] \<Rightarrow> 's certificate"
   "make_cert step phi B \<equiv> 
-     map (\<lambda>pc. if is_target step phi pc then phi!pc else B) [0..length phi(] @ [B]"
+     map (\<lambda>pc. if is_target step phi pc then phi!pc else B) [0..<length phi] @ [B]"
 
 constdefs
   list_ex :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool"
@@ -26,7 +26,7 @@
 
 lemma [code]:
   "is_target step phi pc' =
-  list_ex (\<lambda>pc. pc' \<noteq> pc+1 \<and> pc' mem (map fst (step pc (phi!pc)))) [0..length phi(]"
+  list_ex (\<lambda>pc. pc' \<noteq> pc+1 \<and> pc' mem (map fst (step pc (phi!pc)))) [0..<length phi]"
   apply (simp add: list_ex_def is_target_def set_mem_eq)
   apply force
   done