# HG changeset patch # User haftmann # Date 1248960091 -7200 # Node ID 55ca0df19af587078b90431879d27f57204c5e64 # Parent 605877054de7343dc6b68a3863c97544c741bebf more appropriate printing of function terms diff -r 605877054de7 -r 55ca0df19af5 src/HOL/Code_Eval.thy --- a/src/HOL/Code_Eval.thy Thu Jul 30 15:21:18 2009 +0200 +++ b/src/HOL/Code_Eval.thy Thu Jul 30 15:21:31 2009 +0200 @@ -39,6 +39,17 @@ subsubsection {* @{text term_of} instances *} +instantiation "fun" :: (typerep, typerep) term_of +begin + +definition + "term_of (f \ 'a \ 'b) = Const (STR ''dummy_pattern'') (Typerep.Typerep (STR ''fun'') + [Typerep.typerep TYPE('a), Typerep.typerep TYPE('b)])" + +instance .. + +end + setup {* let fun add_term_of tyco raw_vs thy = diff -r 605877054de7 -r 55ca0df19af5 src/HOL/Tools/quickcheck_generators.ML --- a/src/HOL/Tools/quickcheck_generators.ML Thu Jul 30 15:21:18 2009 +0200 +++ b/src/HOL/Tools/quickcheck_generators.ML Thu Jul 30 15:21:31 2009 +0200 @@ -40,9 +40,10 @@ let val fun_upd = Const (@{const_name fun_upd}, (T1 --> T2) --> T1 --> T2 --> T1 --> T2); - val (seed', seed'') = random_split seed; + val ((y, t2), seed') = random seed; + val (seed'', seed''') = random_split seed'; - val state = ref (seed', [], fn () => Const (@{const_name undefined}, T1 --> T2)); + val state = ref (seed'', [], fn () => Abs ("x", T1, t2 ())); fun random_fun' x = let val (seed, fun_map, f_t) = ! state; @@ -57,7 +58,7 @@ in y end end; fun term_fun' () = #3 (! state) (); - in ((random_fun', term_fun'), seed'') end; + in ((random_fun', term_fun'), seed''') end; (** type copies **)