1.1 --- a/src/Tools/Code/code_thingol.ML	Wed Sep 07 11:36:39 2011 +0200
     1.2 +++ b/src/Tools/Code/code_thingol.ML	Wed Sep 07 13:51:30 2011 +0200
     1.3 @@ -22,7 +22,7 @@
     1.4    datatype itype =
     1.5        `%% of string * itype list
     1.6      | ITyVar of vname;
     1.7 -  type const = string * ((itype list * dict list list) * itype list)
     1.8 +  type const = string * (((itype list * dict list list) * itype list) * bool)
     1.9      (* f [T1..Tn] {dicts} (_::S1) .. (_..Sm) =^= (f, (([T1..Tn], dicts), [S1..Sm]) *)
    1.10    datatype iterm =
    1.11        IConst of const
    1.12 @@ -145,7 +145,8 @@
    1.13      `%% of string * itype list
    1.14    | ITyVar of vname;
    1.15  
    1.16 -type const = string * ((itype list * dict list list) * itype list (*types of arguments*))
    1.17 +type const = string * (((itype list * dict list list) * itype list (*types of arguments*))
    1.18 +  * bool (*requires type annotation*))
    1.19  
    1.20  datatype iterm =
    1.21      IConst of const
    1.22 @@ -198,7 +199,7 @@
    1.23  fun add_tycos (tyco `%% tys) = insert (op =) tyco #> fold add_tycos tys
    1.24    | add_tycos (ITyVar _) = I;
    1.25  
    1.26 -val add_tyconames = fold_constexprs (fn (_, ((tys, _), _)) => fold add_tycos tys);
    1.27 +val add_tyconames = fold_constexprs (fn (_, (((tys, _), _), _)) => fold add_tycos tys);
    1.28  
    1.29  fun fold_varnames f =
    1.30    let
    1.31 @@ -240,7 +241,7 @@
    1.32          val vs_tys = (map o apfst) SOME (Name.invent_names ctxt "a" tys);
    1.33        in (vs_tys, t `$$ map (IVar o fst) vs_tys) end;
    1.34  
    1.35 -fun eta_expand k (c as (name, (_, tys)), ts) =
    1.36 +fun eta_expand k (c as (name, ((_, tys), _)), ts) =
    1.37    let
    1.38      val j = length ts;
    1.39      val l = k - j;
    1.40 @@ -256,7 +257,7 @@
    1.41      fun cont_dict (Dict (_, d)) = cont_plain_dict d
    1.42      and cont_plain_dict (Dict_Const (_, dss)) = (exists o exists) cont_dict dss
    1.43        | cont_plain_dict (Dict_Var _) = true;
    1.44 -    fun cont_term (IConst (_, ((_, dss), _))) = (exists o exists) cont_dict dss
    1.45 +    fun cont_term (IConst (_, (((_, dss), _), _))) = (exists o exists) cont_dict dss
    1.46        | cont_term (IVar _) = false
    1.47        | cont_term (t1 `$ t2) = cont_term t1 orelse cont_term t2
    1.48        | cont_term (_ `|=> t) = cont_term t
    1.49 @@ -756,7 +757,8 @@
    1.50      ##>> fold_map (translate_typ thy algbr eqngr permissive) arg_typs
    1.51      ##>> fold_map (translate_dicts thy algbr eqngr permissive some_thm) (arg_typs ~~ sorts)
    1.52      ##>> fold_map (translate_typ thy algbr eqngr permissive) function_typs
    1.53 -    #>> (fn (((c, arg_typs), dss), function_typs) => IConst (c, ((arg_typs, dss), function_typs)))
    1.54 +    #>> (fn (((c, arg_typs), dss), function_typs) =>
    1.55 +      IConst (c, (((arg_typs, dss), function_typs), false))) (* FIXME *)
    1.56    end
    1.57  and translate_app_const thy algbr eqngr permissive some_thm ((c_ty, ts), some_abs) =
    1.58    translate_const thy algbr eqngr permissive some_thm (c_ty, some_abs)
    1.59 @@ -801,7 +803,7 @@
    1.60          val ts_clause = nth_drop t_pos ts;
    1.61          val clauses = if null case_pats
    1.62            then mk_clause (fn ([t], body) => (t, body)) [ty] (the_single ts_clause)
    1.63 -          else maps (fn ((constr as IConst (_, (_, tys)), n), t) =>
    1.64 +          else maps (fn ((constr as IConst (_, ((_, tys), _)), n), t) =>
    1.65              mk_clause (fn (ts, body) => (constr `$$ ts, body)) (take n tys) t)
    1.66                (constrs ~~ ts_clause);
    1.67        in ((t, ty), clauses) end;