diff -r 95df565aceb7 -r e46e7a9cb622 src/HOL/Tools/quickcheck_generators.ML --- a/src/HOL/Tools/quickcheck_generators.ML Thu Aug 26 13:44:50 2010 +0200 +++ b/src/HOL/Tools/quickcheck_generators.ML Thu Aug 26 20:51:17 2010 +0200 @@ -342,7 +342,7 @@ val bound_max = length Ts - 1; val bounds = map_index (fn (i, ty) => (2 * (bound_max - i) + 1, 2 * (bound_max - i), 2 * i, ty)) Ts; - fun strip_imp (Const(@{const_name "op -->"},_) $ A $ B) = apfst (cons A) (strip_imp B) + fun strip_imp (Const(@{const_name HOL.implies},_) $ A $ B) = apfst (cons A) (strip_imp B) | strip_imp A = ([], A) val prop' = betapplys (prop, map (fn (i, _, _, _) => Bound i) bounds); val terms = HOLogic.mk_list @{typ term} (map (fn (_, i, _, _) => Bound i $ @{term "()"}) bounds)