src/HOL/Tools/quickcheck_generators.ML
changeset 38786 e46e7a9cb622
parent 38553 56965d8e4e11
child 39252 8f176e575a49
--- 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)