diff -r 39d5d42116c4 -r 00bed5ac9884 src/HOL/MicroJava/BV/Opt.thy
--- a/src/HOL/MicroJava/BV/Opt.thy	Tue Jan 16 08:06:55 2007 +0100
+++ b/src/HOL/MicroJava/BV/Opt.thy	Tue Jan 16 08:06:57 2007 +0100
@@ -54,7 +54,7 @@
 
 lemma order_le_opt [intro!,simp]:
   "order r \<Longrightarrow> order(le r)"
-apply (subst order_def)
+apply (subst Semilat.order_def)
 apply (blast intro: le_opt_refl le_opt_trans le_opt_antisym)
 done