diff -r 4dc65845eab3 -r d8d7d1b785af src/HOL/MicroJava/DFA/LBVComplete.thy
--- a/src/HOL/MicroJava/DFA/LBVComplete.thy	Wed Feb 24 11:55:52 2010 +0100
+++ b/src/HOL/MicroJava/DFA/LBVComplete.thy	Mon Mar 01 13:40:23 2010 +0100
@@ -9,12 +9,11 @@
 imports LBVSpec Typing_Framework
 begin
 
-constdefs
-  is_target :: "['s step_type, 's list, nat] \<Rightarrow> bool" 
+definition is_target :: "['s step_type, 's list, nat] \<Rightarrow> bool" where 
   "is_target step phi pc' \<equiv>
      \<exists>pc s'. pc' \<noteq> pc+1 \<and> pc < length phi \<and> (pc',s') \<in> set (step pc (phi!pc))"
 
-  make_cert :: "['s step_type, 's list, 's] \<Rightarrow> 's certificate"
+definition make_cert :: "['s step_type, 's list, 's] \<Rightarrow> 's certificate" where
   "make_cert step phi B \<equiv> 
      map (\<lambda>pc. if is_target step phi pc then phi!pc else B) [0..<length phi] @ [B]"