Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/pattern.ML
changeset 52179 3b9c31867707
parent 52133 f8cd46077224
child 52220 c4264f71dc3b 
--- a/src/Pure/pattern.ML	Mon May 27 15:57:38 2013 +0200
+++ b/src/Pure/pattern.ML	Mon May 27 16:52:39 2013 +0200
@@ -242,8 +242,15 @@
 
 and cases thy (binders,env,(s,t)) = case (strip_comb s,strip_comb t) of
        ((Var(F,Fty),ss),(Var(G,Gty),ts)) =>
-         if F = G then flexflex1(env,binders,F,Fty,ints_of' env ss,ints_of' env ts)
-                  else flexflex2(env,binders,F,Fty,ints_of' env ss,G,Gty,ints_of' env ts)
+          if F = G then
+            let val env' = unify_types thy (Fty, Gty) env
+            in flexflex1(env',binders,F,Fty,ints_of' env' ss,ints_of' env' ts) end
+          else
+            let val env' =
+              unify_types thy
+               (Envir.body_type env (length ss) Fty,
+                Envir.body_type env (length ts) Gty) env
+            in flexflex2(env',binders,F,Fty,ints_of' env' ss,G,Gty,ints_of' env' ts) end
       | ((Var(F,Fty),ss),_)           => flexrigid thy (env,binders,F,Fty,ints_of' env ss,t)
       | (_,(Var(F,Fty),ts))           => flexrigid thy (env,binders,F,Fty,ints_of' env ts,s)
       | ((Const c,ss),(Const d,ts))   => rigidrigid thy (env,binders,c,d,ss,ts)
isabelle