Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
exception handling
authorpaulson
Mon, 02 Apr 2007 11:29:44 +0200
changeset 22559 b824487d9b41
parent 22558 c233923bbabe
child 22560 f19ddf96c323
exception handling
src/Pure/consts.ML file | annotate | diff | comparison | revisions 
--- 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)]);
isabelle