diff -r 7ecb4124a3a3 -r 26b19918e670 src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Wed Sep 07 13:51:34 2011 +0200
+++ b/src/Tools/Code/code_thingol.ML	Wed Sep 07 13:51:35 2011 +0200
@@ -786,16 +786,17 @@
         then translation_error thy permissive some_thm
           "Abstraction violation" ("constant " ^ Code.string_of_const thy c)
       else ()
-    val arg_typs = Sign.const_typargs thy (c, ty);
+    val (annotate, ty') = (case ty of Type("", [ty']) => (true, ty') | ty' => (false, ty'))
+    val arg_typs = Sign.const_typargs thy (c, ty');
     val sorts = Code_Preproc.sortargs eqngr c;
-    val (function_typs, body_typ) = Term.strip_type ty;
+    val (function_typs, body_typ) = Term.strip_type ty';
   in
     ensure_const thy algbr eqngr permissive c
     ##>> fold_map (translate_typ thy algbr eqngr permissive) arg_typs
     ##>> fold_map (translate_dicts thy algbr eqngr permissive some_thm) (arg_typs ~~ sorts)
     ##>> fold_map (translate_typ thy algbr eqngr permissive) (body_typ :: function_typs)
     #>> (fn (((c, arg_typs), dss), body_typ :: function_typs) =>
-      IConst (c, (((arg_typs, dss), (function_typs, body_typ)), false))) (* FIXME *)
+      IConst (c, (((arg_typs, dss), (function_typs, body_typ)), annotate)))
   end
 and translate_app_const thy algbr eqngr permissive some_thm ((c_ty, ts), some_abs) =
   translate_const thy algbr eqngr permissive some_thm (c_ty, some_abs)