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 52220 c4264f71dc3b
parent 52179 3b9c31867707
child 52709 0e4bacf21e77 
--- a/src/Pure/pattern.ML	Wed May 29 11:06:38 2013 +0200
+++ b/src/Pure/pattern.ML	Wed May 29 11:53:31 2013 +0200
@@ -242,15 +242,8 @@
 
 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
-            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
+         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)
       | ((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