diff -r 4dc65845eab3 -r d8d7d1b785af src/HOL/MicroJava/Comp/TranslComp.thy
--- a/src/HOL/MicroJava/Comp/TranslComp.thy	Wed Feb 24 11:55:52 2010 +0100
+++ b/src/HOL/MicroJava/Comp/TranslComp.thy	Mon Mar 01 13:40:23 2010 +0100
@@ -98,17 +98,16 @@
 (*compiling methods, classes and programs*) 
 
 (*initialising a single variable*)
-constdefs
- load_default_val :: "ty => instr"
+definition load_default_val :: "ty => instr" where
 "load_default_val ty == LitPush (default_val ty)"
 
- compInit :: "java_mb => (vname * ty) => instr list"
+definition compInit :: "java_mb => (vname * ty) => instr list" where
 "compInit jmb == \<lambda> (vn,ty). [load_default_val ty, Store (index jmb vn)]"
 
- compInitLvars :: "[java_mb, (vname \<times> ty) list] \<Rightarrow> bytecode"
+definition compInitLvars :: "[java_mb, (vname \<times> ty) list] \<Rightarrow> bytecode" where
  "compInitLvars jmb lvars == concat (map (compInit jmb) lvars)"
 
-  compMethod :: "java_mb prog \<Rightarrow> cname \<Rightarrow> java_mb mdecl \<Rightarrow> jvm_method mdecl"
+definition compMethod :: "java_mb prog \<Rightarrow> cname \<Rightarrow> java_mb mdecl \<Rightarrow> jvm_method mdecl" where
   "compMethod G C jmdl == let (sig, rT, jmb) = jmdl;
                         (pns,lvars,blk,res) = jmb;
                         mt = (compTpMethod G C jmdl);
@@ -117,10 +116,10 @@
                              [Return]
                   in (sig, rT, max_ssize mt, length lvars, bc, [])"
 
-  compClass :: "java_mb prog => java_mb cdecl=> jvm_method cdecl"
+definition compClass :: "java_mb prog => java_mb cdecl=> jvm_method cdecl" where
   "compClass G == \<lambda> (C,cno,fdls,jmdls). (C,cno,fdls, map (compMethod G C) jmdls)"
 
-  comp :: "java_mb prog => jvm_prog"
+definition comp :: "java_mb prog => jvm_prog" where
   "comp G == map (compClass G) G"
 
 end