# HG changeset patch
# User paulson
# Date 1290178751 0
# Node ID 7202d63bfffefd789821d8fea76d5992011f1ad2
# Parent  c5ee1e06d79548e17c3e3eab6cb004ffbf7146ed# Parent  4a1173d21ec41d8564b59057bb8c653ad71ee2e9
merged

diff -r c5ee1e06d795 -r 7202d63bfffe src/Pure/pattern.ML
--- a/src/Pure/pattern.ML	Fri Nov 19 14:35:58 2010 +0100
+++ b/src/Pure/pattern.ML	Fri Nov 19 14:59:11 2010 +0000
@@ -365,6 +365,7 @@
   and cases(binders,env as (iTs,itms),pat,obj) =
     let val (ph,pargs) = strip_comb pat
         fun rigrig1(iTs,oargs) = fold (mtch binders) (pargs~~oargs) (iTs,itms)
+				 handle UnequalLengths => raise MATCH
         fun rigrig2((a:string,Ta),(b,Tb),oargs) =
               if a <> b then raise MATCH
               else rigrig1(typ_match thy (Ta,Tb) iTs, oargs)