# HG changeset patch
# User bulwahn
# Date 1297090018 -3600
# Node ID 91c2510e19c5263d4480fb42d963f75bd354b8df
# Parent  3422ae5aff3a351a7f7bbc0097400f84cb055413
improving term construction of product types in Smallcheck which enables correct presentation of counterexamples

diff -r 3422ae5aff3a -r 91c2510e19c5 src/HOL/Smallcheck.thy
--- a/src/HOL/Smallcheck.thy	Sat Feb 05 20:38:32 2011 +0100
+++ b/src/HOL/Smallcheck.thy	Mon Feb 07 15:46:58 2011 +0100
@@ -113,7 +113,12 @@
 
 definition
   "full_small f d = full_small (%(x, t1). full_small (%(y, t2). f ((x, y),
-    %u. Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.term_of (Pair :: 'a => 'b => ('a * 'b))) (t1 ())) (t2 ()))) d) d"
+    %u. let T1 = (Typerep.typerep (TYPE('a)));
+            T2 = (Typerep.typerep (TYPE('b)))
+    in Code_Evaluation.App (Code_Evaluation.App (
+      Code_Evaluation.Const (STR ''Product_Type.Pair'') 
+      (Typerep.Typerep (STR ''fun'') [T1, Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''Product_Type.prod'') [T1, T2]]]))
+      (t1 ())) (t2 ()))) d) d"
 
 instance ..
 
@@ -229,11 +234,23 @@
 begin
 
 definition
-  "check_all f = check_all (%(x, t1). check_all (%(y, t2). f ((x, y), %_. Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.term_of (Pair :: 'a => 'b => ('a * 'b))) (t1 ())) (t2 ()))))"
+  "check_all f = check_all (%(x, t1). check_all (%(y, t2). f ((x, y),
+    %u. let T1 = (Typerep.typerep (TYPE('a)));
+            T2 = (Typerep.typerep (TYPE('b)))
+    in Code_Evaluation.App (Code_Evaluation.App (
+      Code_Evaluation.Const (STR ''Product_Type.Pair'') 
+      (Typerep.Typerep (STR ''fun'') [T1, Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''Product_Type.prod'') [T1, T2]]]))
+      (t1 ())) (t2 ()))))"
 
 definition enum_term_of_prod :: "('a * 'b) itself => unit => term list"
 where
-  "enum_term_of_prod = (%_ _. map (%(x, y). Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.term_of (Pair :: 'a => 'b => ('a * 'b))) x) y) (Enum.product (enum_term_of (TYPE('a)) ()) (enum_term_of (TYPE('b)) ())))"
+  "enum_term_of_prod = (%_ _. map (%(x, y).
+       let T1 = (Typerep.typerep (TYPE('a)));
+           T2 = (Typerep.typerep (TYPE('b)))
+       in Code_Evaluation.App (Code_Evaluation.App (
+         Code_Evaluation.Const (STR ''Product_Type.Pair'') 
+           (Typerep.Typerep (STR ''fun'') [T1, Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''Product_Type.prod'') [T1, T2]]])) x) y)
+     (Enum.product (enum_term_of (TYPE('a)) ()) (enum_term_of (TYPE('b)) ())))  "
 
 instance ..