--- a/src/HOL/Tools/hologic.ML Wed May 13 18:41:36 2009 +0200
+++ b/src/HOL/Tools/hologic.ML Wed May 13 18:41:38 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;
--- a/src/HOL/ex/Quickcheck_Generators.thy Wed May 13 18:41:36 2009 +0200
+++ b/src/HOL/ex/Quickcheck_Generators.thy Wed May 13 18:41:38 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}