diff -r 4dc65845eab3 -r d8d7d1b785af src/HOL/MicroJava/BV/Altern.thy
--- a/src/HOL/MicroJava/BV/Altern.thy	Wed Feb 24 11:55:52 2010 +0100
+++ b/src/HOL/MicroJava/BV/Altern.thy	Mon Mar 01 13:40:23 2010 +0100
@@ -8,19 +8,18 @@
 imports BVSpec
 begin
 
-constdefs
-  check_type :: "jvm_prog \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> JVMType.state \<Rightarrow> bool"
+definition check_type :: "jvm_prog \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> JVMType.state \<Rightarrow> bool" where
   "check_type G mxs mxr s \<equiv> s \<in> states G mxs mxr"
 
-  wt_instr_altern :: "[instr,jvm_prog,ty,method_type,nat,nat,p_count,
-                exception_table,p_count] \<Rightarrow> bool"
+definition wt_instr_altern :: "[instr,jvm_prog,ty,method_type,nat,nat,p_count,
+                exception_table,p_count] \<Rightarrow> bool" where
   "wt_instr_altern i G rT phi mxs mxr max_pc et pc \<equiv>
   app i G mxs rT pc et (phi!pc) \<and>
   check_type G mxs mxr (OK (phi!pc)) \<and>
   (\<forall>(pc',s') \<in> set (eff i G pc et (phi!pc)). pc' < max_pc \<and> G \<turnstile> s' <=' phi!pc')"
 
-  wt_method_altern :: "[jvm_prog,cname,ty list,ty,nat,nat,instr list,
-                 exception_table,method_type] \<Rightarrow> bool"
+definition wt_method_altern :: "[jvm_prog,cname,ty list,ty,nat,nat,instr list,
+                 exception_table,method_type] \<Rightarrow> bool" where
   "wt_method_altern G C pTs rT mxs mxl ins et phi \<equiv>
   let max_pc = length ins in
   0 < max_pc \<and>