--- a/src/HOL/MicroJava/Comp/Index.thy Wed Feb 24 11:55:52 2010 +0100
+++ b/src/HOL/MicroJava/Comp/Index.thy Mon Mar 01 13:40:23 2010 +0100
@@ -9,8 +9,7 @@
begin
(*indexing a variable name among all variable declarations in a method body*)
-constdefs
- index :: "java_mb => vname => nat"
+definition index :: "java_mb => vname => nat" where
"index == \<lambda> (pn,lv,blk,res) v.
if v = This
then 0
@@ -99,8 +98,7 @@
(* The following def should replace the conditions in WellType.thy / wf_java_mdecl
*)
-constdefs
- disjoint_varnames :: "[vname list, (vname \<times> ty) list] \<Rightarrow> bool"
+definition disjoint_varnames :: "[vname list, (vname \<times> ty) list] \<Rightarrow> bool" where
(* This corresponds to the original def in wf_java_mdecl:
"disjoint_varnames pns lvars \<equiv>
nodups pns \<and> unique lvars \<and> This \<notin> set pns \<and> This \<notin> set (map fst lvars) \<and>