src/HOL/Quickcheck.thy
changeset 44845 5e51075cbd97
parent 42175 32c3bb5e1b1a
child 45159 3f1d1ce024cb
--- a/src/HOL/Quickcheck.thy	Thu Sep 08 08:41:28 2011 -0700
+++ b/src/HOL/Quickcheck.thy	Fri Sep 09 00:22:18 2011 +0200
@@ -183,7 +183,7 @@
 where
   "union R1 R2 = (\<lambda>s. let
      (P1, s') = R1 s; (P2, s'') = R2 s'
-   in (semilattice_sup_class.sup P1 P2, s''))"
+   in (sup_class.sup P1 P2, s''))"
 
 definition if_randompred :: "bool \<Rightarrow> unit randompred"
 where