src/HOL/MicroJava/BV/Kildall.thy
changeset 11299 1d3d110c456e
parent 11298 acd83fa66e92
child 11549 e7265e70fd7c
--- a/src/HOL/MicroJava/BV/Kildall.thy	Mon May 14 09:58:22 2001 +0200
+++ b/src/HOL/MicroJava/BV/Kildall.thy	Wed May 16 12:31:25 2001 +0200
@@ -349,7 +349,7 @@
       pres_type step n A; bounded succs n; 
       mono r step n A |]
   ==> is_bcv r T step succs n A (kildall r f step succs)"
-apply(unfold is_bcv_def welltyping_def)
+apply(unfold is_bcv_def wt_step_def)
 apply(insert kildall_properties[of A])
 apply(simp add:stables_def)
 apply clarify