--- a/src/HOL/Tools/quickcheck_generators.ML Thu Aug 19 10:27:12 2010 +0200
+++ b/src/HOL/Tools/quickcheck_generators.ML Thu Aug 19 11:02:14 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("op -->",_) $ A $ B) = apfst (cons A) (strip_imp B)
+ fun strip_imp (Const(@{const_name "op -->"},_) $ 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)