src/HOL/Tools/hologic.ML

   val mk_string: string -> term
   val dest_string: term -> string
   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 =
 struct
 

       $ mk_string s;
 fun dest_message_string (Const ("String.message_string.STR", _) $ t) =
       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;