# HG changeset patch
# User haftmann
# Date 1279281466 -7200
# Node ID ff1c9cb6dc5d17e7c736f8d26cdbe68fb6460712
# Parent  a3632a0b7d6ceb432c56a430796164c774ba46a7
don't fail gracefully

diff -r a3632a0b7d6c -r ff1c9cb6dc5d src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Fri Jul 16 13:57:29 2010 +0200
+++ b/src/Tools/Code/code_thingol.ML	Fri Jul 16 13:57:46 2010 +0200
@@ -222,10 +222,12 @@
         val vs_tys = (map o apfst) SOME (Name.names ctxt "a" tys);
       in (vs_tys, t `$$ map (IVar o fst) vs_tys) end;
 
-fun eta_expand k (c as (_, (_, tys)), ts) =
+fun eta_expand k (c as (name, (_, tys)), ts) =
   let
     val j = length ts;
     val l = k - j;
+    val _ = if l > length tys
+      then error ("Impossible eta-expansion for constant " ^ quote name) else ();
     val ctxt = (fold o fold_varnames) Name.declare ts Name.context;
     val vs_tys = (map o apfst) SOME
       (Name.names ctxt "a" ((take l o drop j) tys));