src/HOL/Code_Evaluation.thy

 in
   Code.datatype_interpretation ensure_term_of_code
 end
 *}
 
+setup {*
+let
+  fun mk_term_of_eq thy ty vs tyco abs ty_rep proj =
+    let
+      val arg = Var (("x", 0), ty);
+      val rhs = Abs ("y", @{typ term}, HOLogic.reflect_term (Const (abs, ty_rep --> ty) $ Bound 0)) $
+        (HOLogic.mk_term_of ty_rep (Const (proj, ty --> ty_rep) $ arg))
+        |> Thm.cterm_of thy;
+      val cty = Thm.ctyp_of thy ty;
+    in
+      @{thm term_of_anything}
+      |> Drule.instantiate' [SOME cty] [SOME (Thm.cterm_of thy arg), SOME rhs]
+      |> Thm.varifyT
+    end;
+  fun add_term_of_code tyco raw_vs abs raw_ty_rep proj thy =
+    let
+      val algebra = Sign.classes_of thy;
+      val vs = map (fn (v, sort) =>
+        (v, curry (Sorts.inter_sort algebra) @{sort typerep} sort)) raw_vs;
+      val ty = Type (tyco, map TFree vs);
+      val ty_rep = map_atyps
+        (fn TFree (v, _) => TFree (v, (the o AList.lookup (op =) vs) v)) raw_ty_rep;
+      val const = AxClass.param_of_inst thy (@{const_name term_of}, tyco);
+      val eq = mk_term_of_eq thy ty vs tyco abs ty_rep proj;
+   in
+      thy
+      |> Code.del_eqns const
+      |> Code.add_eqn eq
+    end;
+  fun ensure_term_of_code (tyco, (raw_vs, ((abs, ty), (proj, _)))) thy =
+    let
+      val has_inst = can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of};
+    in if has_inst then add_term_of_code tyco raw_vs abs ty proj thy else thy end;
+in
+  Code.abstype_interpretation ensure_term_of_code
+end
+*}
+
 
 subsubsection {* Code generator setup *}
 
 lemmas [code del] = term.recs term.cases term.size
 lemma [code, code del]: "eq_class.eq (t1\<Colon>term) t2 \<longleftrightarrow> eq_class.eq t1 t2" ..