1.1 --- a/src/Tools/Code/code_thingol.ML	Wed Sep 07 13:51:34 2011 +0200
     1.2 +++ b/src/Tools/Code/code_thingol.ML	Wed Sep 07 13:51:35 2011 +0200
     1.3 @@ -786,16 +786,17 @@
     1.4          then translation_error thy permissive some_thm
     1.5            "Abstraction violation" ("constant " ^ Code.string_of_const thy c)
     1.6        else ()
     1.7 -    val arg_typs = Sign.const_typargs thy (c, ty);
     1.8 +    val (annotate, ty') = (case ty of Type("", [ty']) => (true, ty') | ty' => (false, ty'))
     1.9 +    val arg_typs = Sign.const_typargs thy (c, ty');
    1.10      val sorts = Code_Preproc.sortargs eqngr c;
    1.11 -    val (function_typs, body_typ) = Term.strip_type ty;
    1.12 +    val (function_typs, body_typ) = Term.strip_type ty';
    1.13    in
    1.14      ensure_const thy algbr eqngr permissive c
    1.15      ##>> fold_map (translate_typ thy algbr eqngr permissive) arg_typs
    1.16      ##>> fold_map (translate_dicts thy algbr eqngr permissive some_thm) (arg_typs ~~ sorts)
    1.17      ##>> fold_map (translate_typ thy algbr eqngr permissive) (body_typ :: function_typs)
    1.18      #>> (fn (((c, arg_typs), dss), body_typ :: function_typs) =>
    1.19 -      IConst (c, (((arg_typs, dss), (function_typs, body_typ)), false))) (* FIXME *)
    1.20 +      IConst (c, (((arg_typs, dss), (function_typs, body_typ)), annotate)))
    1.21    end
    1.22  and translate_app_const thy algbr eqngr permissive some_thm ((c_ty, ts), some_abs) =
    1.23    translate_const thy algbr eqngr permissive some_thm (c_ty, some_abs)