diff -r 4dc65845eab3 -r d8d7d1b785af src/HOL/Bali/Trans.thy
--- a/src/HOL/Bali/Trans.thy	Wed Feb 24 11:55:52 2010 +0100
+++ b/src/HOL/Bali/Trans.thy	Mon Mar 01 13:40:23 2010 +0100
@@ -9,7 +9,7 @@
 
 theory Trans imports Evaln begin
 
-constdefs groundVar:: "var \<Rightarrow> bool"
+definition groundVar :: "var \<Rightarrow> bool" where
 "groundVar v \<equiv> (case v of
                    LVar ln \<Rightarrow> True
                  | {accC,statDeclC,stat}e..fn \<Rightarrow> \<exists> a. e=Lit a
@@ -34,7 +34,7 @@
     done
 qed
 
-constdefs groundExprs:: "expr list \<Rightarrow> bool"
+definition groundExprs :: "expr list \<Rightarrow> bool" where
 "groundExprs es \<equiv> list_all (\<lambda> e. \<exists> v. e=Lit v) es"
   
 consts the_val:: "expr \<Rightarrow> val"