# 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 \<Colon> 'a \<Rightarrow> '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 **)