don't fail gracefully
authorhaftmann
Fri Jul 16 13:57:46 2010 +0200 (2010-07-16)
changeset 37841ff1c9cb6dc5d
parent 37840 a3632a0b7d6c
child 37843 336dae59af03
don't fail gracefully
src/Tools/Code/code_thingol.ML
     1.1 --- a/src/Tools/Code/code_thingol.ML	Fri Jul 16 13:57:29 2010 +0200
     1.2 +++ b/src/Tools/Code/code_thingol.ML	Fri Jul 16 13:57:46 2010 +0200
     1.3 @@ -222,10 +222,12 @@
     1.4          val vs_tys = (map o apfst) SOME (Name.names ctxt "a" tys);
     1.5        in (vs_tys, t `$$ map (IVar o fst) vs_tys) end;
     1.6  
     1.7 -fun eta_expand k (c as (_, (_, tys)), ts) =
     1.8 +fun eta_expand k (c as (name, (_, tys)), ts) =
     1.9    let
    1.10      val j = length ts;
    1.11      val l = k - j;
    1.12 +    val _ = if l > length tys
    1.13 +      then error ("Impossible eta-expansion for constant " ^ quote name) else ();
    1.14      val ctxt = (fold o fold_varnames) Name.declare ts Name.context;
    1.15      val vs_tys = (map o apfst) SOME
    1.16        (Name.names ctxt "a" ((take l o drop j) tys));