diff -r a11a1e4e0403 -r 97e7d9c189db src/HOL/Tools/typecopy.ML
--- a/src/HOL/Tools/typecopy.ML	Tue Aug 17 15:29:41 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,123 +0,0 @@
-(*  Title:      HOL/Tools/typecopy.ML
-    Author:     Florian Haftmann, TU Muenchen
-
-Introducing copies of types using trivial typedefs; datatype-like abstraction.
-*)
-
-signature TYPECOPY =
-sig
-  type info = { vs: (string * sort) list, typ: typ, constr: string, proj: string,
-    constr_inject: thm, proj_inject: thm, constr_proj: thm, proj_constr: thm }
-  val typecopy: binding * (string * sort) list -> typ -> binding -> binding
-    -> theory -> (string * info) * theory
-  val get_info: theory -> string -> info option
-  val add_default_code: string -> theory -> theory
-end;
-
-structure Typecopy: TYPECOPY =
-struct
-
-(* theory data *)
-
-type info = {
-  vs: (string * sort) list,
-  typ: typ,
-  constr: string,
-  proj: string,
-  constr_inject: thm,
-  proj_inject: thm,
-  constr_proj: thm,
-  proj_constr: thm
-};
-
-structure Typecopy_Data = Theory_Data
-(
-  type T = info Symtab.table;
-  val empty = Symtab.empty;
-  val extend = I;
-  fun merge data = Symtab.merge (K true) data;
-);
-
-val get_info = Symtab.lookup o Typecopy_Data.get;
-
-
-(* default code setup *)
-
-fun add_default_code tyco thy =
-  let
-    val SOME { vs, typ = ty_rep, constr = c, proj, proj_constr, proj_inject, ... } =
-      get_info thy tyco;
-    val constr = (c, Logic.unvarifyT_global (Sign.the_const_type thy c));
-    val ty = Type (tyco, map TFree vs);
-    val proj = Const (proj, ty --> ty_rep);
-    val (t_x, t_y) = (Free ("x", ty), Free ("y", ty));
-    val eq_lhs = Const (@{const_name eq_class.eq}, ty --> ty --> HOLogic.boolT)
-      $ t_x $ t_y;
-    val eq_rhs = HOLogic.mk_eq (proj $ t_x, proj $ t_y);
-    val eq = (HOLogic.mk_Trueprop o HOLogic.mk_eq) (eq_lhs, eq_rhs);
-    fun tac eq_thm = Class.intro_classes_tac []
-      THEN (Simplifier.rewrite_goals_tac
-        (map Simpdata.mk_eq [eq_thm, @{thm eq}, proj_inject]))
-          THEN ALLGOALS (rtac @{thm refl});
-    fun mk_eq_refl thy = @{thm HOL.eq_refl}
-      |> Thm.instantiate
-         ([pairself (Thm.ctyp_of thy) (TVar (("'a", 0), @{sort eq}), Logic.varifyT_global ty)], [])
-      |> AxClass.unoverload thy;
-  in
-    thy
-    |> Code.add_datatype [constr]
-    |> Code.add_eqn proj_constr
-    |> Class.instantiation ([tyco], vs, [HOLogic.class_eq])
-    |> `(fn lthy => Syntax.check_term lthy eq)
-    |-> (fn eq => Specification.definition
-         (NONE, (Attrib.empty_binding, eq)))
-    |-> (fn (_, (_, eq_thm)) =>
-       Class.prove_instantiation_exit_result Morphism.thm
-         (fn _ => fn eq_thm => tac eq_thm) eq_thm)
-    |-> (fn eq_thm => Code.add_eqn eq_thm)
-    |> (fn thy => Code.add_nbe_eqn (mk_eq_refl thy) thy)
-  end;
-
-
-(* 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;