# HG changeset patch
# User haftmann
# Date 1281628601 -7200
# Node ID 7c045c03598f6eb3e175e8c83b068eb918cb9f5b
# Parent  8a3ca8b96b23270dd072bc1c5e1ca4e55cc6cdd1
group record-related ML files

diff -r 8a3ca8b96b23 -r 7c045c03598f src/HOL/Main.thy
--- a/src/HOL/Main.thy	Thu Aug 12 13:53:42 2010 +0200
+++ b/src/HOL/Main.thy	Thu Aug 12 17:56:41 2010 +0200
@@ -1,7 +1,7 @@
 header {* Main HOL *}
 
 theory Main
-imports Plain Predicate_Compile Nitpick SMT
+imports Plain Record Predicate_Compile Nitpick SMT
 begin
 
 text {*
diff -r 8a3ca8b96b23 -r 7c045c03598f src/HOL/Nitpick.thy
--- a/src/HOL/Nitpick.thy	Thu Aug 12 13:53:42 2010 +0200
+++ b/src/HOL/Nitpick.thy	Thu Aug 12 17:56:41 2010 +0200
@@ -8,7 +8,7 @@
 header {* Nitpick: Yet Another Counterexample Generator for Isabelle/HOL *}
 
 theory Nitpick
-imports Map Quotient SAT
+imports Map Quotient SAT Record
 uses ("Tools/Nitpick/kodkod.ML")
      ("Tools/Nitpick/kodkod_sat.ML")
      ("Tools/Nitpick/nitpick_util.ML")
diff -r 8a3ca8b96b23 -r 7c045c03598f src/HOL/Plain.thy
--- a/src/HOL/Plain.thy	Thu Aug 12 13:53:42 2010 +0200
+++ b/src/HOL/Plain.thy	Thu Aug 12 17:56:41 2010 +0200
@@ -1,7 +1,7 @@
 header {* Plain HOL *}
 
 theory Plain
-imports Datatype Record FunDef Extraction
+imports Datatype FunDef Extraction
 begin
 
 text {*
diff -r 8a3ca8b96b23 -r 7c045c03598f src/HOL/Tools/quickcheck_generators.ML
--- a/src/HOL/Tools/quickcheck_generators.ML	Thu Aug 12 13:53:42 2010 +0200
+++ b/src/HOL/Tools/quickcheck_generators.ML	Thu Aug 12 17:56:41 2010 +0200
@@ -10,7 +10,6 @@
   val random_fun: typ -> typ -> ('a -> 'a -> bool) -> ('a -> term)
     -> (seed -> ('b * (unit -> term)) * seed) -> (seed -> seed * seed)
     -> seed -> (('a -> 'b) * (unit -> term)) * seed
-  val ensure_random_typecopy: string -> theory -> theory
   val random_aux_specification: string -> string -> term list -> local_theory -> local_theory
   val mk_random_aux_eqs: theory -> Datatype.descr -> (string * sort) list
     -> string list -> string list * string list -> typ list * typ list
@@ -65,53 +64,10 @@
   in ((random_fun', term_fun'), seed''') end;
 
 
-(** type copies **)
-
-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 thy =
-  let
-    val SOME { vs = raw_vs, constr, typ = raw_T, ... } =
-      Typecopy.get_info thy tyco;
-    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;
-
-
 (** datatypes **)
 
 (* definitional scheme for random instances on datatypes *)
 
-(*FIXME avoid this low-level proving*)
 local
 
 fun dest_ctyp_nth k cT = nth (Thm.dest_ctyp cT) k;
@@ -450,8 +406,8 @@
 
 (** setup **)
 
-val setup = Typecopy.interpretation ensure_random_typecopy
-  #> Datatype.interpretation ensure_random_datatype
+val setup =
+  Datatype.interpretation ensure_random_datatype
   #> Code_Target.extend_target (target, (Code_Eval.target, K I))
   #> Quickcheck.add_generator ("code", compile_generator_expr o ProofContext.theory_of);
 
diff -r 8a3ca8b96b23 -r 7c045c03598f src/HOL/Typedef.thy
--- a/src/HOL/Typedef.thy	Thu Aug 12 13:53:42 2010 +0200
+++ b/src/HOL/Typedef.thy	Thu Aug 12 17:56:41 2010 +0200
@@ -8,7 +8,6 @@
 imports Set
 uses
   ("Tools/typedef.ML")
-  ("Tools/typecopy.ML")
   ("Tools/typedef_codegen.ML")
 begin
 
@@ -116,7 +115,6 @@
 end
 
 use "Tools/typedef.ML" setup Typedef.setup
-use "Tools/typecopy.ML" setup Typecopy.setup
 use "Tools/typedef_codegen.ML" setup TypedefCodegen.setup
 
 end