# HG changeset patch
# User haftmann
# Date 1242240497 -7200
# Node ID 570eaf57cd4d9e556f60eecada55387bd88b6aa3
# Parent  d9752181691aede31b090d9646d34b66de0d93e5# Parent  e5f8c1c420f3bade7ed2f643b35c43140289723f
merged

diff -r d9752181691a -r 570eaf57cd4d src/HOL/Code_Eval.thy
--- a/src/HOL/Code_Eval.thy	Wed May 13 17:13:33 2009 +0100
+++ b/src/HOL/Code_Eval.thy	Wed May 13 20:48:17 2009 +0200
@@ -28,30 +28,15 @@
 lemma term_of_anything: "term_of x \<equiv> t"
   by (rule eq_reflection) (cases "term_of x", cases t, simp)
 
-ML {*
-structure Eval =
-struct
-
-fun mk_term f g (Const (c, ty)) =
-      @{term Const} $ HOLogic.mk_message_string c $ g ty
-  | mk_term f g (t1 $ t2) =
-      @{term App} $ mk_term f g t1 $ mk_term f g t2
-  | mk_term f g (Free v) = f v
-  | mk_term f g (Bound i) = Bound i
-  | mk_term f g (Abs (v, _, t)) = Abs (v, @{typ term}, mk_term f g t);
-
-fun mk_term_of ty t = Const (@{const_name term_of}, ty --> @{typ term}) $ t;
-
-end;
-*}
-
 
 subsubsection {* @{text term_of} instances *}
 
 setup {*
 let
-  fun add_term_of_def ty vs tyco thy =
+  fun add_term_of tyco raw_vs thy =
     let
+      val vs = map (fn (v, _) => (v, @{sort typerep})) raw_vs;
+      val ty = Type (tyco, map TFree vs);
       val lhs = Const (@{const_name term_of}, ty --> @{typ term})
         $ Free ("x", ty);
       val rhs = @{term "undefined \<Colon> term"};
@@ -64,66 +49,59 @@
       |> `(fn lthy => Syntax.check_term lthy eq)
       |-> (fn eq => Specification.definition (NONE, ((Binding.name (triv_name_of eq), []), eq)))
       |> snd
-      |> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
-      |> LocalTheory.exit_global
+      |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
     end;
-  fun interpretator ("prop", (raw_vs, _)) thy = thy
-    | interpretator (tyco, (raw_vs, _)) thy =
-        let
-          val has_inst = can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of};
-          val constrain_sort =
-            curry (Sorts.inter_sort (Sign.classes_of thy)) @{sort term_of};
-          val vs = (map o apsnd) constrain_sort raw_vs;
-          val ty = Type (tyco, map TFree vs);
-        in
-          thy
-          |> Typerep.perhaps_add_def tyco
-          |> not has_inst ? add_term_of_def ty vs tyco
-        end;
+  fun ensure_term_of (tyco, (raw_vs, _)) thy =
+    let
+      val need_inst = not (can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of})
+        andalso can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort typerep};
+    in
+      thy
+      |> need_inst ? add_term_of tyco raw_vs
+    end;
 in
-  Code.type_interpretation interpretator
+  Code.type_interpretation ensure_term_of
 end
 *}
 
 setup {*
 let
-  fun mk_term_of_eq ty vs tyco (c, tys) =
+  fun mk_term_of_eq thy ty vs tyco (c, tys) =
     let
       val t = list_comb (Const (c, tys ---> ty),
         map Free (Name.names Name.context "a" tys));
-    in (map_aterms (fn Free (v, ty) => Var ((v, 0), ty) | t => t) t, Eval.mk_term
-      (fn (v, ty) => Eval.mk_term_of ty (Var ((v, 0), ty)))
-      (Typerep.mk (fn (v, sort) => Typerep.typerep (TFree (v, sort)))) t)
+      val (arg, rhs) = pairself (Thm.cterm_of thy o map_types Logic.unvarifyT o Logic.varify)
+        (t, (map_aterms (fn t as Free (v, ty) => HOLogic.mk_term_of ty t | t => t) o HOLogic.reflect_term) t)
+        handle TYPE (msg, tys, ts) => (tracing msg; error "")
+      val cty = Thm.ctyp_of thy ty;
+      val _ = tracing (cat_lines [makestring arg, makestring rhs, makestring cty])
+    in
+      @{thm term_of_anything}
+      |> Drule.instantiate' [SOME cty] [SOME arg, SOME rhs]
+      |> Thm.varifyT
     end;
-  fun prove_term_of_eq ty eq thy =
+  fun add_term_of_code tyco raw_vs raw_cs thy =
     let
-      val cty = Thm.ctyp_of thy ty;
-      val (arg, rhs) = pairself (Thm.cterm_of thy) eq;
-      val thm = @{thm term_of_anything}
-        |> Drule.instantiate' [SOME cty] [SOME arg, SOME rhs]
-        |> Thm.varifyT;
+      val vs = map (fn (v, _) => (v, @{sort typerep})) raw_vs;
+      val ty = Type (tyco, map TFree vs);
+      val cs = (map o apsnd o map o map_atyps)
+        (fn TFree (v, _) => TFree (v, (the o AList.lookup (op =) vs) v)) raw_cs;
+      val const = AxClass.param_of_inst thy (@{const_name term_of}, tyco);
+      val eqs = map (mk_term_of_eq thy ty vs tyco) cs;
+   in
+      thy
+      |> Code.del_eqns const
+      |> fold Code.add_eqn eqs
+    end;
+  fun ensure_term_of_code (tyco, (raw_vs, cs)) thy =
+    let
+      val has_inst = can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of};
     in
       thy
-      |> Code.add_eqn thm
+      |> has_inst ? add_term_of_code tyco raw_vs cs
     end;
-  fun interpretator ("prop", (raw_vs, _)) thy = thy
-    | interpretator (tyco, (raw_vs, raw_cs)) thy =
-        let
-          val constrain_sort =
-            curry (Sorts.inter_sort (Sign.classes_of thy)) @{sort term_of};
-          val vs = (map o apsnd) constrain_sort raw_vs;
-          val cs = (map o apsnd o map o map_atyps)
-            (fn TFree (v, sort) => TFree (v, constrain_sort sort)) raw_cs;
-          val ty = Type (tyco, map TFree vs);
-          val eqs = map (mk_term_of_eq ty vs tyco) cs;
-          val const = AxClass.param_of_inst thy (@{const_name term_of}, tyco);
-        in
-          thy
-          |> Code.del_eqns const
-          |> fold (prove_term_of_eq ty) eqs
-        end;
 in
-  Code.type_interpretation interpretator
+  Code.type_interpretation ensure_term_of_code
 end
 *}
 
@@ -164,8 +142,6 @@
 ML {*
 signature EVAL =
 sig
-  val mk_term: ((string * typ) -> term) -> (typ -> term) -> term -> term
-  val mk_term_of: typ -> term -> term
   val eval_ref: (unit -> term) option ref
   val eval_term: theory -> term -> term
 end;
@@ -173,14 +149,10 @@
 structure Eval : EVAL =
 struct
 
-open Eval;
-
 val eval_ref = ref (NONE : (unit -> term) option);
 
 fun eval_term thy t =
-  t 
-  |> Eval.mk_term_of (fastype_of t)
-  |> (fn t => Code_ML.eval NONE ("Eval.eval_ref", eval_ref) I thy t []);
+  Code_ML.eval NONE ("Eval.eval_ref", eval_ref) I thy (HOLogic.mk_term_of (fastype_of t) t) [];
 
 end;
 *}
diff -r d9752181691a -r 570eaf57cd4d src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Wed May 13 17:13:33 2009 +0100
+++ b/src/HOL/HOL.thy	Wed May 13 20:48:17 2009 +0200
@@ -1836,6 +1836,22 @@
 
 lemmas [code, code unfold, symmetric, code post] = imp_conv_disj
 
+instantiation itself :: (type) eq
+begin
+
+definition eq_itself :: "'a itself \<Rightarrow> 'a itself \<Rightarrow> bool" where
+  "eq_itself x y \<longleftrightarrow> x = y"
+
+instance proof
+qed (fact eq_itself_def)
+
+end
+
+lemma eq_itself_code [code]:
+  "eq_class.eq TYPE('a) TYPE('a) \<longleftrightarrow> True"
+  by (simp add: eq)
+
+
 text {* Equality *}
 
 declare simp_thms(6) [code nbe]
diff -r d9752181691a -r 570eaf57cd4d src/HOL/Predicate.thy
--- a/src/HOL/Predicate.thy	Wed May 13 17:13:33 2009 +0100
+++ b/src/HOL/Predicate.thy	Wed May 13 20:48:17 2009 +0200
@@ -610,7 +610,7 @@
     (simp_all add: Seq_def single_less_eq_eval contained_less_eq)
 
 lemma eq_pred_code [code]:
-  fixes P Q :: "'a::eq pred"
+  fixes P Q :: "'a pred"
   shows "eq_class.eq P Q \<longleftrightarrow> P \<le> Q \<and> Q \<le> P"
   unfolding eq by auto
 
diff -r d9752181691a -r 570eaf57cd4d src/HOL/Tools/datatype_codegen.ML
--- a/src/HOL/Tools/datatype_codegen.ML	Wed May 13 17:13:33 2009 +0100
+++ b/src/HOL/Tools/datatype_codegen.ML	Wed May 13 20:48:17 2009 +0200
@@ -6,7 +6,7 @@
 
 signature DATATYPE_CODEGEN =
 sig
-  val mk_eq: theory -> string -> thm list
+  val mk_eq_eqns: theory -> string -> (thm * bool) list
   val mk_case_cert: theory -> string -> thm
   val setup: theory -> theory
 end;
@@ -309,18 +309,6 @@
 
 (** generic code generator **)
 
-(* specification *)
-
-fun add_datatype_spec vs dtco cos thy =
-  let
-    val cs = map (fn (c, tys) => (c, tys ---> Type (dtco, map TFree vs))) cos;
-  in
-    thy
-    |> try (Code.add_datatype cs)
-    |> the_default thy
-  end;
-
-
 (* case certificates *)
 
 fun mk_case_cert thy tyco =
@@ -354,88 +342,41 @@
     |> Thm.varifyT
   end;
 
-fun add_datatype_cases dtco thy =
-  let
-    val {case_rewrites, ...} = DatatypePackage.the_datatype thy dtco;
-    val cert = mk_case_cert thy dtco;
-    fun add_case_liberal thy = thy
-      |> try (Code.add_case cert)
-      |> the_default thy;
-  in
-    thy
-    |> add_case_liberal
-    |> fold_rev Code.add_default_eqn case_rewrites
-  end;
-
 
 (* equality *)
 
-local
-
-val not_sym = @{thm HOL.not_sym};
-val not_false_true = iffD2 OF [nth @{thms HOL.simp_thms} 7, TrueI];
-val refl = @{thm refl};
-val eqTrueI = @{thm eqTrueI};
-
-fun mk_distinct cos =
-  let
-    fun sym_product [] = []
-      | sym_product (x::xs) = map (pair x) xs @ sym_product xs;
-    fun mk_co_args (co, tys) ctxt =
-      let
-        val names = Name.invents ctxt "a" (length tys);
-        val ctxt' = fold Name.declare names ctxt;
-        val vs = map2 (curry Free) names tys;
-      in (vs, ctxt') end;
-    fun mk_dist ((co1, tys1), (co2, tys2)) =
-      let
-        val ((xs1, xs2), _) = Name.context
-          |> mk_co_args (co1, tys1)
-          ||>> mk_co_args (co2, tys2);
-        val prem = HOLogic.mk_eq
-          (list_comb (co1, xs1), list_comb (co2, xs2));
-        val t = HOLogic.mk_not prem;
-      in HOLogic.mk_Trueprop t end;
-  in map mk_dist (sym_product cos) end;
-
-in
-
-fun mk_eq thy dtco =
+fun mk_eq_eqns thy dtco =
   let
-    val (vs, cs) = DatatypePackage.the_datatype_spec thy dtco;
-    fun mk_triv_inject co =
-      let
-        val ct' = Thm.cterm_of thy
-          (Const (co, Type (dtco, map (fn (v, sort) => TVar ((v, 0), sort)) vs)))
-        val cty' = Thm.ctyp_of_term ct';
-        val SOME (ct, cty) = fold_aterms (fn Var (v, ty) =>
-          (K o SOME) (Thm.cterm_of thy (Var (v, Thm.typ_of cty')), Thm.ctyp_of thy ty) | _ => I)
-          (Thm.prop_of refl) NONE;
-      in eqTrueI OF [Thm.instantiate ([(cty, cty')], [(ct, ct')]) refl] end;
-    val inject1 = map_filter (fn (co, []) => SOME (mk_triv_inject co) | _ => NONE) cs
-    val inject2 = (#inject o DatatypePackage.the_datatype thy) dtco;
-    val ctxt = ProofContext.init thy;
-    val simpset = Simplifier.context ctxt
-      (Simplifier.empty_ss addsimprocs [DatatypePackage.distinct_simproc]);
-    val cos = map (fn (co, tys) =>
-        (Const (co, tys ---> Type (dtco, map TFree vs)), tys)) cs;
-    val tac = ALLGOALS (simp_tac simpset)
-      THEN ALLGOALS (ProofContext.fact_tac [not_false_true, TrueI]);
-    val distinct =
-      mk_distinct cos
-      |> map (fn t => Goal.prove_global thy [] [] t (K tac))
-      |> (fn thms => thms @ map (fn thm => not_sym OF [thm]) thms)
-  in inject1 @ inject2 @ distinct end;
+    val (vs, cos) = DatatypePackage.the_datatype_spec thy dtco;
+    val { descr, index, inject = inject_thms, ... } = DatatypePackage.the_datatype thy dtco;
+    val ty = Type (dtco, map TFree vs);
+    fun mk_eq (t1, t2) = Const (@{const_name eq_class.eq}, ty --> ty --> HOLogic.boolT)
+      $ t1 $ t2;
+    fun true_eq t12 = HOLogic.mk_eq (mk_eq t12, HOLogic.true_const);
+    fun false_eq t12 = HOLogic.mk_eq (mk_eq t12, HOLogic.false_const);
+    val triv_injects = map_filter
+     (fn (c, []) => SOME (HOLogic.mk_Trueprop (true_eq (Const (c, ty), Const (c, ty))))
+       | _ => NONE) cos;
+    fun prep_inject (trueprop $ (equiv $ (_ $ t1 $ t2) $ rhs)) =
+      trueprop $ (equiv $ mk_eq (t1, t2) $ rhs);
+    val injects = map prep_inject (nth (DatatypeProp.make_injs [descr] vs) index);
+    fun prep_distinct (trueprop $ (not $ (_ $ t1 $ t2))) =
+      [trueprop $ false_eq (t1, t2), trueprop $ false_eq (t2, t1)];
+    val distincts = maps prep_distinct (snd (nth (DatatypeProp.make_distincts [descr] vs) index));
+    val refl = HOLogic.mk_Trueprop (true_eq (Free ("x", ty), Free ("x", ty)));
+    val simpset = Simplifier.context (ProofContext.init thy) (HOL_basic_ss
+      addsimps (map Simpdata.mk_eq (@{thm eq} :: @{thm eq_True} :: inject_thms))
+      addsimprocs [DatatypePackage.distinct_simproc]);
+    fun prove prop = Goal.prove_global thy [] [] prop (K (ALLGOALS (simp_tac simpset)))
+      |> Simpdata.mk_eq
+      |> Simplifier.rewrite_rule [@{thm equals_eq}];
+  in map (rpair true o prove) (triv_injects @ injects @ distincts) @ [(prove refl, false)] end;
 
-end;
-
-fun add_datatypes_equality vs dtcos thy =
+fun add_equality vs dtcos thy =
   let
-    val vs' = (map o apsnd)
-      (curry (Sorts.inter_sort (Sign.classes_of thy)) [HOLogic.class_eq]) vs;
     fun add_def dtco lthy =
       let
-        val ty = Type (dtco, map TFree vs');
+        val ty = Type (dtco, map TFree vs);
         fun mk_side const_name = Const (const_name, ty --> ty --> HOLogic.boolT)
           $ Free ("x", ty) $ Free ("y", ty);
         val def = HOLogic.mk_Trueprop (HOLogic.mk_eq
@@ -448,52 +389,60 @@
       in (thm', lthy') end;
     fun tac thms = Class.intro_classes_tac []
       THEN ALLGOALS (ProofContext.fact_tac thms);
-    fun mk_eq' thy dtco = mk_eq thy dtco
-      |> map (Code_Unit.constrain_thm thy [HOLogic.class_eq])
-      |> map Simpdata.mk_eq
-      |> map (MetaSimplifier.rewrite_rule [Thm.transfer thy @{thm equals_eq}])
-      |> map (AxClass.unoverload thy);
     fun add_eq_thms dtco thy =
       let
-        val ty = Type (dtco, map TFree vs');
+        val const = AxClass.param_of_inst thy (@{const_name eq_class.eq}, dtco);
         val thy_ref = Theory.check_thy thy;
-        val const = AxClass.param_of_inst thy (@{const_name eq_class.eq}, dtco);
-        val eq_refl = @{thm HOL.eq_refl}
-          |> Thm.instantiate
-              ([pairself (Thm.ctyp_of thy) (TVar (("'a", 0), @{sort eq}), Logic.varifyT ty)], [])
-          |> Simpdata.mk_eq
-          |> AxClass.unoverload thy;
-        fun mk_thms () = (eq_refl, false)
-          :: rev (map (rpair true) (mk_eq' (Theory.deref thy_ref) dtco));
+        fun mk_thms () = rev ((mk_eq_eqns (Theory.deref thy_ref) dtco));
       in
         Code.add_eqnl (const, Lazy.lazy mk_thms) thy
       end;
   in
     thy
-    |> TheoryTarget.instantiation (dtcos, vs', [HOLogic.class_eq])
+    |> TheoryTarget.instantiation (dtcos, vs, [HOLogic.class_eq])
     |> fold_map add_def dtcos
-    |-> (fn thms => Class.prove_instantiation_instance (K (tac thms))
-    #> LocalTheory.exit_global
-    #> fold Code.del_eqn thms
-    #> fold add_eq_thms dtcos)
+    |-> (fn def_thms => Class.prove_instantiation_exit_result (map o Morphism.thm)
+         (fn _ => fn def_thms => tac def_thms) def_thms)
+    |-> (fn def_thms => fold Code.del_eqn def_thms)
+    |> fold add_eq_thms dtcos
+  end;
+
+
+(* liberal addition of code data for datatypes *)
+
+fun mk_constr_consts thy vs dtco cos =
+  let
+    val cs = map (fn (c, tys) => (c, tys ---> Type (dtco, map TFree vs))) cos;
+    val cs' = map (fn c_ty as (_, ty) => (AxClass.unoverload_const thy c_ty, ty)) cs;
+  in if is_some (try (Code_Unit.constrset_of_consts thy) cs')
+    then SOME cs
+    else NONE
   end;
 
+fun add_all_code dtcos thy =
+  let
+    val (vs :: _, coss) = (split_list o map (DatatypePackage.the_datatype_spec thy)) dtcos;
+    val any_css = map2 (mk_constr_consts thy vs) dtcos coss;
+    val css = if exists is_none any_css then []
+      else map_filter I any_css;
+    val case_rewrites = maps (#case_rewrites o DatatypePackage.the_datatype thy) dtcos;
+    val certs = map (mk_case_cert thy) dtcos;
+  in
+    if null css then thy
+    else thy
+      |> fold Code.add_datatype css
+      |> fold_rev Code.add_default_eqn case_rewrites
+      |> fold Code.add_case certs
+      |> add_equality vs dtcos
+   end;
+
+
 
 (** theory setup **)
 
-fun add_datatype_code dtcos thy =
-  let
-    val (vs :: _, coss) = (split_list o map (DatatypePackage.the_datatype_spec thy)) dtcos;
-  in
-    thy
-    |> fold2 (add_datatype_spec vs) dtcos coss
-    |> fold add_datatype_cases dtcos
-    |> add_datatypes_equality vs dtcos
-  end;
-
 val setup = 
   add_codegen "datatype" datatype_codegen
   #> add_tycodegen "datatype" datatype_tycodegen
-  #> DatatypePackage.interpretation add_datatype_code
+  #> DatatypePackage.interpretation add_all_code
 
 end;
diff -r d9752181691a -r 570eaf57cd4d src/HOL/Tools/hologic.ML
--- a/src/HOL/Tools/hologic.ML	Wed May 13 17:13:33 2009 +0100
+++ b/src/HOL/Tools/hologic.ML	Wed May 13 20:48:17 2009 +0200
@@ -119,6 +119,9 @@
   val message_stringT: typ
   val mk_message_string: string -> term
   val dest_message_string: term -> string
+  val mk_typerep: typ -> term
+  val mk_term_of: typ -> term -> term
+  val reflect_term: term -> term
 end;
 
 structure HOLogic: HOLOGIC =
@@ -591,4 +594,26 @@
       dest_string t
   | dest_message_string t = raise TERM ("dest_message_string", [t]);
 
+
+(* typerep and term *)
+
+val typerepT = Type ("Typerep.typerep", []);
+
+fun mk_typerep T = Const ("Typerep.typerep_class.typerep",
+  Term.itselfT T --> typerepT) $ Logic.mk_type T;
+
+val termT = Type ("Code_Eval.term", []);
+
+fun mk_term_of T t = Const ("Code_Eval.term_of_class.term_of", T --> termT) $ t;
+
+fun reflect_term (Const (c, T)) =
+      Const ("Code_Eval.Const", message_stringT --> typerepT --> termT)
+        $ mk_message_string c $ mk_typerep T
+  | reflect_term (t1 $ t2) =
+      Const ("Code_Eval.App", termT --> termT --> termT)
+        $ reflect_term t1 $ reflect_term t2
+  | reflect_term (t as Free _) = t
+  | reflect_term (t as Bound _) = t
+  | reflect_term (Abs (v, _, t)) = Abs (v, termT, reflect_term t);
+
 end;
diff -r d9752181691a -r 570eaf57cd4d src/HOL/Tools/record_package.ML
--- a/src/HOL/Tools/record_package.ML	Wed May 13 17:13:33 2009 +0100
+++ b/src/HOL/Tools/record_package.ML	Wed May 13 20:48:17 2009 +0200
@@ -1464,7 +1464,7 @@
     val tname = Binding.name (Long_Name.base_name name);
   in
     thy
-    |> TypecopyPackage.add_typecopy (Binding.suffix_name ext_typeN tname, alphas) repT NONE
+    |> TypecopyPackage.typecopy (Binding.suffix_name ext_typeN tname, alphas) repT NONE
     |-> (fn (name, _) => `(fn thy => get_thms thy name))
   end;
 
diff -r d9752181691a -r 570eaf57cd4d src/HOL/Tools/typecopy_package.ML
--- a/src/HOL/Tools/typecopy_package.ML	Wed May 13 17:13:33 2009 +0100
+++ b/src/HOL/Tools/typecopy_package.ML	Wed May 13 20:48:17 2009 +0200
@@ -14,12 +14,12 @@
     proj: string * typ,
     proj_def: thm
   }
-  val add_typecopy: binding * string list -> typ -> (binding * binding) option
+  val typecopy: binding * string list -> typ -> (binding * binding) option
     -> theory -> (string * info) * theory
   val get_typecopies: theory -> string list
   val get_info: theory -> string -> info option
   val interpretation: (string -> theory -> theory) -> theory -> theory
-  val add_typecopy_default_code: string -> theory -> theory
+  val add_default_code: string -> theory -> theory
   val print_typecopies: theory -> unit
   val setup: theory -> theory
 end;
@@ -71,7 +71,10 @@
 structure TypecopyInterpretation = InterpretationFun(type T = string val eq = op =);
 val interpretation = TypecopyInterpretation.interpretation;
 
-fun add_typecopy (raw_tyco, raw_vs) raw_ty constr_proj thy =
+
+(* declaring typecopies *)
+
+fun typecopy (raw_tyco, raw_vs) raw_ty constr_proj thy =
   let
     val ty = Sign.certify_typ thy raw_ty;
     val vs =
@@ -108,28 +111,26 @@
   end;
 
 
-(* code generator setup *)
+(* default code setup *)
 
-fun add_typecopy_default_code tyco thy =
+fun add_default_code tyco thy =
   let
     val SOME { constr = constr_name, proj = (proj, _), proj_def = proj_eq, vs = raw_vs,
-      typ = raw_ty_rep, ... } =  get_info thy tyco;
-    val inst_meet = Sorts.meet_sort_typ (Sign.classes_of thy)
-      (Logic.varifyT raw_ty_rep, [HOLogic.class_eq]) handle Sorts.CLASS_ERROR _ => I;
-    val ty_inst = Logic.unvarifyT o inst_meet o Logic.varifyT;
-    val vs = (map dest_TFree o snd o dest_Type o ty_inst)
-      (Type (tyco, map TFree raw_vs));
-    val ty_rep = ty_inst raw_ty_rep;
+      typ = ty_rep, ... } =  get_info thy tyco;
     val SOME { Rep_inject = proj_inject, ... } = TypedefPackage.get_info thy tyco;
-    val ty_constr = Logic.unvarifyT (Sign.the_const_type thy constr_name);
-    val constr = (constr_name, ty_constr)
+    val constr = (constr_name, Logic.unvarifyT (Sign.the_const_type thy constr_name));
+    val vs = (map dest_TFree o snd o dest_Type) (Type (tyco, map TFree raw_vs));
     val ty = Type (tyco, map TFree vs);
-    fun mk_eq ty t_x t_y = Const (@{const_name eq_class.eq}, ty --> ty --> HOLogic.boolT)
+    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;
-    fun mk_proj t = Const (proj, ty --> ty_rep) $ t;
-    val (t_x, t_y) = (Free ("x", ty), Free ("y", ty));
-    val def_eq = (HOLogic.mk_Trueprop o HOLogic.mk_eq)
-      (mk_eq ty t_x t_y, HOLogic.mk_eq (mk_proj t_x, mk_proj 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 ty)], [])
@@ -139,22 +140,18 @@
     |> Code.add_datatype [constr]
     |> Code.add_eqn proj_eq
     |> TheoryTarget.instantiation ([tyco], vs, [HOLogic.class_eq])
-    |> `(fn lthy => Syntax.check_term lthy def_eq)
-    |-> (fn def_eq => Specification.definition
-         (NONE, (Attrib.empty_binding, def_eq)))
-    |-> (fn (_, (_, def_thm)) =>
+    |> `(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 def_thm => Class.intro_classes_tac []
-            THEN (Simplifier.rewrite_goals_tac
-              (map Simpdata.mk_eq [def_thm, @{thm eq}, proj_inject]))
-                THEN ALLGOALS (rtac @{thm refl})) def_thm)
-    |-> (fn def_thm => Code.add_eqn def_thm)
-    |> `(fn thy => mk_eq_refl thy)
-    |-> (fn refl_thm => Code.add_nbe_eqn refl_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;
 
 val setup =
   TypecopyInterpretation.init
-  #> interpretation add_typecopy_default_code
+  #> interpretation add_default_code
 
 end;
diff -r d9752181691a -r 570eaf57cd4d src/HOL/Typerep.thy
--- a/src/HOL/Typerep.thy	Wed May 13 17:13:33 2009 +0100
+++ b/src/HOL/Typerep.thy	Wed May 13 20:48:17 2009 +0200
@@ -35,28 +35,18 @@
 end
 *}
 
-ML {*
-structure Typerep =
-struct
+setup {*
+let
 
-fun mk f (Type (tyco, tys)) =
-      @{term Typerep} $ HOLogic.mk_message_string tyco
-        $ HOLogic.mk_list @{typ typerep} (map (mk f) tys)
-  | mk f (TFree v) =
-      f v;
-
-fun typerep ty =
-  Const (@{const_name typerep}, Term.itselfT ty --> @{typ typerep})
-    $ Logic.mk_type ty;
-
-fun add_def tyco thy =
+fun add_typerep tyco thy =
   let
     val sorts = replicate (Sign.arity_number thy tyco) @{sort typerep};
     val vs = Name.names Name.context "'a" sorts;
     val ty = Type (tyco, map TFree vs);
     val lhs = Const (@{const_name typerep}, Term.itselfT ty --> @{typ typerep})
       $ Free ("T", Term.itselfT ty);
-    val rhs = mk (typerep o TFree) ty;
+    val rhs = @{term Typerep} $ HOLogic.mk_message_string tyco
+      $ HOLogic.mk_list @{typ typerep} (map (HOLogic.mk_typerep o TFree) vs);
     val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
   in
     thy
@@ -64,23 +54,20 @@
     |> `(fn lthy => Syntax.check_term lthy eq)
     |-> (fn eq => Specification.definition (NONE, (Attrib.empty_binding, eq)))
     |> snd
-    |> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
-    |> LocalTheory.exit_global
+    |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
   end;
 
-fun perhaps_add_def tyco thy =
-  let
-    val inst = can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort typerep}
-  in if inst then thy else add_def tyco thy end;
+fun ensure_typerep tyco thy = if not (can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort typerep})
+  andalso can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort type}
+  then add_typerep tyco thy else thy;
+
+in
 
-end;
-*}
+add_typerep @{type_name fun}
+#> TypedefPackage.interpretation ensure_typerep
+#> Code.type_interpretation (ensure_typerep o fst)
 
-setup {*
-  Typerep.add_def @{type_name fun}
-  #> Typerep.add_def @{type_name itself}
-  #> Typerep.add_def @{type_name bool}
-  #> TypedefPackage.interpretation Typerep.perhaps_add_def
+end
 *}
 
 lemma [code]:
diff -r d9752181691a -r 570eaf57cd4d src/HOL/ex/Predicate_Compile.thy
--- a/src/HOL/ex/Predicate_Compile.thy	Wed May 13 17:13:33 2009 +0100
+++ b/src/HOL/ex/Predicate_Compile.thy	Wed May 13 20:48:17 2009 +0200
@@ -22,9 +22,7 @@
 val pred_ref = ref (NONE : (unit -> term Predicate.pred) option);
 
 fun eval_pred thy t =
-  t 
-  |> Eval.mk_term_of (fastype_of t)
-  |> (fn t => Code_ML.eval NONE ("Predicate.pred_ref", pred_ref) @{code pred_map} thy t []);
+  Code_ML.eval NONE ("Predicate.pred_ref", pred_ref) @{code pred_map} thy (HOLogic.mk_term_of (fastype_of t) t) [];
 
 fun eval_pred_elems thy t T length =
   t |> eval_pred thy |> yieldn length |> fst |> HOLogic.mk_list T;
diff -r d9752181691a -r 570eaf57cd4d src/HOL/ex/Quickcheck_Generators.thy
--- a/src/HOL/ex/Quickcheck_Generators.thy	Wed May 13 17:13:33 2009 +0100
+++ b/src/HOL/ex/Quickcheck_Generators.thy	Wed May 13 20:48:17 2009 +0200
@@ -54,7 +54,7 @@
       val t_indices = map (curry ( op * ) 2) (length tys - 1 downto 0);
       val c_indices = map (curry ( op + ) 1) t_indices;
       val c_t = list_comb (c, map Bound c_indices);
-      val t_t = Abs ("", @{typ unit}, Eval.mk_term Free Typerep.typerep
+      val t_t = Abs ("", @{typ unit}, HOLogic.reflect_term
         (list_comb (c, map (fn k => Bound (k + 1)) t_indices))
         |> map_aterms (fn t as Bound _ => t $ @{term "()"} | t => t));
       val return = StateMonad.return (term_ty this_ty) @{typ seed}
diff -r d9752181691a -r 570eaf57cd4d src/HOL/ex/Term_Of_Syntax.thy
--- a/src/HOL/ex/Term_Of_Syntax.thy	Wed May 13 17:13:33 2009 +0100
+++ b/src/HOL/ex/Term_Of_Syntax.thy	Wed May 13 20:48:17 2009 +0200
@@ -31,9 +31,9 @@
 
 setup {*
 let
-  val subst_rterm_of = Eval.mk_term
-    (fn (v, _) => error ("illegal free variable in term quotation: " ^ quote v))
-    (Typerep.mk (fn (v, sort) => Typerep.typerep (TFree (v, sort))));
+  val subst_rterm_of = map_aterms
+    (fn Free (v, _) => error ("illegal free variable in term quotation: " ^ quote v) | t => t)
+      o HOLogic.reflect_term;
   fun subst_rterm_of' (Const (@{const_name rterm_of}, _), [t]) = subst_rterm_of t
     | subst_rterm_of' (Const (@{const_name rterm_of}, _), _) =
         error ("illegal number of arguments for " ^ quote @{const_name rterm_of})
diff -r d9752181691a -r 570eaf57cd4d src/Pure/Isar/code_unit.ML
--- a/src/Pure/Isar/code_unit.ML	Wed May 13 17:13:33 2009 +0100
+++ b/src/Pure/Isar/code_unit.ML	Wed May 13 20:48:17 2009 +0200
@@ -9,7 +9,6 @@
   (*typ instantiations*)
   val typscheme: theory -> string * typ -> (string * sort) list * typ
   val inst_thm: theory -> sort Vartab.table -> thm -> thm
-  val constrain_thm: theory -> sort -> thm -> thm
 
   (*constant aliasses*)
   val add_const_alias: thm -> theory -> theory
@@ -80,15 +79,6 @@
     val insts = map_filter mk_inst tvars;
   in Thm.instantiate (insts, []) thm end;
 
-fun constrain_thm thy sort thm =
-  let
-    val constrain = curry (Sorts.inter_sort (Sign.classes_of thy)) sort
-    val tvars = (Term.add_tvars o Thm.prop_of) thm [];
-    fun mk_inst (tvar as (v, sort)) = pairself (Thm.ctyp_of thy o TVar o pair v)
-      (sort, constrain sort)
-    val insts = map mk_inst tvars;
-  in Thm.instantiate (insts, []) thm end;
-
 fun expand_eta thy k thm =
   let
     val (lhs, rhs) = (Logic.dest_equals o Thm.plain_prop_of) thm;
diff -r d9752181691a -r 570eaf57cd4d src/Tools/quickcheck.ML
--- a/src/Tools/quickcheck.ML	Wed May 13 17:13:33 2009 +0100
+++ b/src/Tools/quickcheck.ML	Wed May 13 20:48:17 2009 +0200
@@ -94,7 +94,7 @@
       error "Term to be tested contains type variables";
     val _ = null (Term.add_vars t []) orelse
       error "Term to be tested contains schematic variables";
-    val frees = map dest_Free (OldTerm.term_frees t);
+    val frees = Term.add_frees t [];
   in (map fst frees, list_abs_free (frees, t)) end
 
 fun test_term ctxt quiet generator_name size i t =