--- a/src/HOL/Library/Eval.thy Sat May 19 11:33:23 2007 +0200
+++ b/src/HOL/Library/Eval.thy Sat May 19 11:33:24 2007 +0200
@@ -34,6 +34,9 @@
end;
*}
+instance int :: typ_of
+ "typ_of T \<equiv> STR ''IntDef.int'' {\<struct>} []" ..
+
setup {*
let
fun mk arities _ thy =