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 =