# HG changeset patch
# User haftmann
# Date 1282050796 -7200
# Node ID bbaaaf6f1cbe4e6c51b77c79bc092bbf6f076c90
# Parent  0e4565062017171717a2a4e19671234e82d542f5
eliminated typecopy interpretation

diff -r 0e4565062017 -r bbaaaf6f1cbe src/HOL/Record.thy
--- a/src/HOL/Record.thy	Tue Aug 17 14:33:44 2010 +0200
+++ b/src/HOL/Record.thy	Tue Aug 17 15:13:16 2010 +0200
@@ -10,7 +10,7 @@
 
 theory Record
 imports Plain Quickcheck
-uses ("Tools/typecopy.ML") ("Tools/record.ML") ("Tools/quickcheck_record.ML")
+uses ("Tools/quickcheck_record.ML") ("Tools/typecopy.ML") ("Tools/record.ML")
 begin
 
 subsection {* Introduction *}
@@ -452,9 +452,9 @@
 
 subsection {* Record package *}
 
-use "Tools/typecopy.ML" setup Typecopy.setup
+use "Tools/quickcheck_record.ML"
+use "Tools/typecopy.ML"
 use "Tools/record.ML" setup Record.setup
-use "Tools/quickcheck_record.ML" setup Quickcheck_Record.setup
 
 hide_const (open) Tuple_Isomorphism repr abst iso_tuple_fst iso_tuple_snd
   iso_tuple_fst_update iso_tuple_snd_update iso_tuple_cons
diff -r 0e4565062017 -r bbaaaf6f1cbe src/HOL/Tools/quickcheck_record.ML
--- a/src/HOL/Tools/quickcheck_record.ML	Tue Aug 17 14:33:44 2010 +0200
+++ b/src/HOL/Tools/quickcheck_record.ML	Tue Aug 17 15:13:16 2010 +0200
@@ -6,8 +6,8 @@
 
 signature QUICKCHECK_RECORD =
 sig
-  val ensure_random_typecopy: string -> theory -> theory
-  val setup: theory -> theory
+  val ensure_random_typecopy: string -> (string * sort) list -> string
+    -> typ -> theory -> theory
 end;
 
 structure Quickcheck_Record : QUICKCHECK_RECORD =
@@ -42,10 +42,8 @@
     |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
   end;
 
-fun ensure_random_typecopy tyco thy =
+fun ensure_random_typecopy tyco raw_vs constr raw_T 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;
@@ -55,6 +53,4 @@
     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;
 
-val setup = Typecopy.interpretation ensure_random_typecopy;
-
 end;
diff -r 0e4565062017 -r bbaaaf6f1cbe src/HOL/Tools/typecopy.ML
--- a/src/HOL/Tools/typecopy.ML	Tue Aug 17 14:33:44 2010 +0200
+++ b/src/HOL/Tools/typecopy.ML	Tue Aug 17 15:13:16 2010 +0200
@@ -11,9 +11,7 @@
   val typecopy: binding * (string * sort) list -> typ -> binding -> binding
     -> theory -> (string * info) * theory
   val get_info: theory -> string -> info option
-  val interpretation: (string -> theory -> theory) -> theory -> theory
   val add_default_code: string -> theory -> theory
-  val setup: theory -> theory
 end;
 
 structure Typecopy: TYPECOPY =
@@ -43,53 +41,6 @@
 val get_info = Symtab.lookup o Typecopy_Data.get;
 
 
-(* interpretation of type copies *)
-
-structure Typecopy_Interpretation = Interpretation(type T = string val eq = op =);
-val interpretation = Typecopy_Interpretation.interpretation;
-
-
-(* introducing typecopies *)
-
-fun add_info tyco vs (({ rep_type, Abs_name, Rep_name, ...},
-    { Abs_inject, Rep_inject, Abs_inverse, Rep_inverse, ... }) : Typedef.info) thy =
-  let
-    val exists_thm =
-      UNIV_I
-      |> Drule.instantiate' [SOME (ctyp_of thy (Logic.varifyT_global rep_type))] [];
-    val constr_inject = Abs_inject OF [exists_thm, exists_thm];
-    val proj_constr = Abs_inverse OF [exists_thm];
-    val info = {
-      vs = vs,
-      typ = rep_type,
-      constr = Abs_name,
-      proj = Rep_name,
-      constr_inject = constr_inject,
-      proj_inject = Rep_inject,
-      constr_proj = Rep_inverse,
-      proj_constr = proj_constr
-    };
-  in
-    thy
-    |> (Typecopy_Data.map o Symtab.update_new) (tyco, info)
-    |> Typecopy_Interpretation.data tyco
-    |> pair (tyco, info)
-  end
-
-fun typecopy (raw_tyco, raw_vs) raw_ty constr proj thy =
-  let
-    val ty = Sign.certify_typ thy raw_ty;
-    val ctxt = ProofContext.init_global thy |> Variable.declare_typ ty;
-    val vs = map (ProofContext.check_tfree ctxt) raw_vs;
-    val tac = Tactic.rtac UNIV_witness 1;
-  in
-    thy
-    |> Typedef.add_typedef_global false (SOME raw_tyco) (raw_tyco, vs, NoSyn)
-      (HOLogic.mk_UNIV ty) (SOME (proj, constr)) tac
-    |-> (fn (tyco, info) => add_info tyco vs info)
-  end;
-
-
 (* default code setup *)
 
 fun add_default_code tyco thy =
@@ -127,8 +78,46 @@
     |> (fn thy => Code.add_nbe_eqn (mk_eq_refl thy) thy)
   end;
 
-val setup =
-  Typecopy_Interpretation.init
-  #> interpretation add_default_code
+
+(* introducing typecopies *)
+
+fun add_info tyco vs (({ rep_type, Abs_name, Rep_name, ...},
+    { Abs_inject, Rep_inject, Abs_inverse, Rep_inverse, ... }) : Typedef.info) thy =
+  let
+    val exists_thm =
+      UNIV_I
+      |> Drule.instantiate' [SOME (ctyp_of thy (Logic.varifyT_global rep_type))] [];
+    val constr_inject = Abs_inject OF [exists_thm, exists_thm];
+    val proj_constr = Abs_inverse OF [exists_thm];
+    val info = {
+      vs = vs,
+      typ = rep_type,
+      constr = Abs_name,
+      proj = Rep_name,
+      constr_inject = constr_inject,
+      proj_inject = Rep_inject,
+      constr_proj = Rep_inverse,
+      proj_constr = proj_constr
+    };
+  in
+    thy
+    |> (Typecopy_Data.map o Symtab.update_new) (tyco, info)
+    |> add_default_code tyco
+    |> Quickcheck_Record.ensure_random_typecopy tyco vs Abs_name rep_type
+    |> pair (tyco, info)
+  end
+
+fun typecopy (raw_tyco, raw_vs) raw_ty constr proj thy =
+  let
+    val ty = Sign.certify_typ thy raw_ty;
+    val ctxt = ProofContext.init_global thy |> Variable.declare_typ ty;
+    val vs = map (ProofContext.check_tfree ctxt) raw_vs;
+    val tac = Tactic.rtac UNIV_witness 1;
+  in
+    thy
+    |> Typedef.add_typedef_global false (SOME raw_tyco) (raw_tyco, vs, NoSyn)
+      (HOLogic.mk_UNIV ty) (SOME (proj, constr)) tac
+    |-> (fn (tyco, info) => add_info tyco vs info)
+  end;
 
 end;