# HG changeset patch
# User haftmann
# Date 1264597372 -3600
# Node ID acd6b305ffb5808b4ba719a578a1205ff24d00b5
# Parent  ceeffca32eb01189edb52390b25438cac1a4c373
corrected type of typecopy constructor

diff -r ceeffca32eb0 -r acd6b305ffb5 src/HOL/Tools/quickcheck_generators.ML
--- a/src/HOL/Tools/quickcheck_generators.ML	Wed Jan 27 14:02:52 2010 +0100
+++ b/src/HOL/Tools/quickcheck_generators.ML	Wed Jan 27 14:02:52 2010 +0100
@@ -65,14 +65,14 @@
 
 fun mk_random_typecopy tyco vs constr T' thy =
   let
+    val mk_const = curry (Sign.mk_const thy);
     val Ts = map TFree vs;  
     val T = Type (tyco, Ts);
     val Tm = termifyT T;
     val Tm' = termifyT T';
-    fun mk_const c Ts = Const (c, Sign.const_instance thy (c, Ts));
     val v = "x";
     val t_v = Free (v, Tm');
-    val t_constr = mk_const constr Ts;
+    val t_constr = Const (constr, T' --> T);
     val lhs = HOLogic.mk_random T size;
     val rhs = HOLogic.mk_ST [((HOLogic.mk_random T' size, @{typ Random.seed}), SOME (v, Tm'))]
       (HOLogic.mk_return Tm @{typ Random.seed}