# HG changeset patch
# User haftmann
# Date 1282143575 -7200
# Node ID 3be65f879bcdd943515bfc3a0634014c52259da5
# Parent  c87b69396a3757e94db08f618b7baf3f429cfde7
removed separate quickcheck_record module

diff -r c87b69396a37 -r 3be65f879bcd src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Wed Aug 18 15:01:57 2010 +0200
+++ b/src/HOL/IsaMakefile	Wed Aug 18 16:59:35 2010 +0200
@@ -302,7 +302,6 @@
   Tools/Predicate_Compile/predicate_compile_specialisation.ML \
   Tools/Predicate_Compile/predicate_compile_pred.ML \
   Tools/quickcheck_generators.ML \
-  Tools/quickcheck_record.ML \
   Tools/Qelim/cooper.ML \
   Tools/Qelim/cooper_procedure.ML \
   Tools/Qelim/qelim.ML \
diff -r c87b69396a37 -r 3be65f879bcd src/HOL/Record.thy
--- a/src/HOL/Record.thy	Wed Aug 18 15:01:57 2010 +0200
+++ b/src/HOL/Record.thy	Wed Aug 18 16:59:35 2010 +0200
@@ -10,7 +10,7 @@
 
 theory Record
 imports Plain Quickcheck
-uses ("Tools/quickcheck_record.ML") ("Tools/record.ML")
+uses ("Tools/record.ML")
 begin
 
 subsection {* Introduction *}
@@ -452,7 +452,6 @@
 
 subsection {* Record package *}
 
-use "Tools/quickcheck_record.ML"
 use "Tools/record.ML" setup Record.setup
 
 hide_const (open) Tuple_Isomorphism repr abst iso_tuple_fst iso_tuple_snd
diff -r c87b69396a37 -r 3be65f879bcd src/HOL/Tools/quickcheck_record.ML
--- a/src/HOL/Tools/quickcheck_record.ML	Wed Aug 18 15:01:57 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,56 +0,0 @@
-(*  Title:      HOL/Tools/quickcheck_record.ML
-    Author:     Florian Haftmann, TU Muenchen
-
-Quickcheck generators for records.
-*)
-
-signature QUICKCHECK_RECORD =
-sig
-  val ensure_random_typecopy: string -> (string * sort) list -> string
-    -> typ -> theory -> theory
-end;
-
-structure Quickcheck_Record : QUICKCHECK_RECORD =
-struct
-
-fun termifyT T = HOLogic.mk_prodT (T, @{typ "unit => term"})
-val size = @{term "i::code_numeral"};
-
-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';
-    val v = "x";
-    val t_v = Free (v, Tm');
-    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}
-      (mk_const "Code_Evaluation.valapp" [T', T]
-        $ HOLogic.mk_prod (t_constr, Abs ("u", @{typ unit}, HOLogic.reflect_term t_constr)) $ t_v))
-      @{typ Random.seed} (SOME Tm, @{typ Random.seed});
-    val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
-  in   
-    thy
-    |> Class.instantiation ([tyco], vs, @{sort random})
-    |> `(fn lthy => Syntax.check_term lthy eq)
-    |-> (fn eq => Specification.definition (NONE, (apfst Binding.conceal Attrib.empty_binding, eq)))
-    |> snd
-    |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
-  end;
-
-fun ensure_random_typecopy tyco raw_vs constr raw_T thy =
-  let
-    val constrain = curry (Sorts.inter_sort (Sign.classes_of thy));
-    val T = map_atyps (fn TFree (v, sort) =>
-      TFree (v, constrain sort @{sort random})) raw_T;
-    val vs' = Term.add_tfreesT T [];
-    val vs = map (fn (v, sort) =>
-      (v, the_default (constrain sort @{sort typerep}) (AList.lookup (op =) vs' v))) raw_vs;
-    val can_inst = Sign.of_sort thy (T, @{sort random});
-  in if can_inst then mk_random_typecopy tyco vs constr T thy else thy end;
-
-end;