diff -r 6a973bd43949 -r 1bc3b688548c src/HOL/MicroJava/BV/BVExample.thy
--- a/src/HOL/MicroJava/BV/BVExample.thy	Wed Dec 02 12:04:07 2009 +0100
+++ b/src/HOL/MicroJava/BV/BVExample.thy	Tue Nov 24 14:37:23 2009 +0100
@@ -66,27 +66,28 @@
 
 text {* The subclass releation spelled out: *}
 lemma subcls1:
-  "subcls1 E = (\<lambda>C D. (C, D) \<in> {(list_name,Object), (test_name,Object), (Xcpt NullPointer, Object),
-                (Xcpt ClassCast, Object), (Xcpt OutOfMemory, Object)})"
+  "subcls1 E = {(list_name,Object), (test_name,Object), (Xcpt NullPointer, Object),
+                (Xcpt ClassCast, Object), (Xcpt OutOfMemory, Object)}"
 apply (simp add: subcls1_def2)
 apply (simp add: name_defs class_defs system_defs E_def class_def)
-apply (auto simp: expand_fun_eq)
+apply (simp add: Sigma_def)
+apply auto
 done
 
 text {* The subclass relation is acyclic; hence its converse is well founded: *}
 lemma notin_rtrancl:
-  "r\<^sup>*\<^sup>* a b \<Longrightarrow> a \<noteq> b \<Longrightarrow> (\<And>y. \<not> r a y) \<Longrightarrow> False"
-  by (auto elim: converse_rtranclpE)
+  "(a, b) \<in> r\<^sup>* \<Longrightarrow> a \<noteq> b \<Longrightarrow> (\<And>y. (a, y) \<notin> r) \<Longrightarrow> False"
+  by (auto elim: converse_rtranclE)
 
-lemma acyclic_subcls1_E: "acyclicP (subcls1 E)"
-  apply (rule acyclicI [to_pred])
+lemma acyclic_subcls1_E: "acyclic (subcls1 E)"
+  apply (rule acyclicI)
   apply (simp add: subcls1)
-  apply (auto dest!: tranclpD)
+  apply (auto dest!: tranclD)
   apply (auto elim!: notin_rtrancl simp add: name_defs distinct_classes)
   done
 
-lemma wf_subcls1_E: "wfP ((subcls1 E)\<inverse>\<inverse>)"
-  apply (rule finite_acyclic_wf_converse [to_pred])
+lemma wf_subcls1_E: "wf ((subcls1 E)\<inverse>)"
+  apply (rule finite_acyclic_wf_converse)
   apply (simp add: subcls1 del: insert_iff)
   apply (rule acyclic_subcls1_E)
   done