# HG changeset patch
# User paulson
# Date 1175506184 -7200
# Node ID b824487d9b411368d81745dbeef1b8b897737624
# Parent  c233923bbabe1614dc89b89ff73d95b04043bb8f
exception handling

diff -r c233923bbabe -r b824487d9b41 src/Pure/consts.ML
--- a/src/Pure/consts.ML	Sun Apr 01 14:28:48 2007 +0200
+++ b/src/Pure/consts.ML	Mon Apr 02 11:29:44 2007 +0200
@@ -189,7 +189,8 @@
   let
     val declT = the_declaration consts c;
     val vars = map Term.dest_TVar (typargs consts (c, declT));
-  in declT |> TermSubst.instantiateT (vars ~~ Ts) end;
+  in declT |> TermSubst.instantiateT (vars ~~ Ts) end
+  handle UnequalLengths => raise TYPE ("const_instance", Ts, [Const(c,dummyT)]);