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.
unify types of bound variables in the same manner as Unify.new_dpair (which emphatically "Tries to unify types of the bound variables!");
authorwenzelm
Fri, 24 May 2013 15:32:02 +0200
changeset 52129 3fd0fe916097
parent 52128 7f3549a316f4
child 52130 86f7d8bc2a5f
unify types of bound variables in the same manner as Unify.new_dpair (which emphatically "Tries to unify types of the bound variables!");
src/Pure/pattern.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/pattern.ML	Fri May 24 15:13:25 2013 +0200
+++ b/src/Pure/pattern.ML	Fri May 24 15:32:02 2013 +0200
@@ -239,7 +239,7 @@
 fun unif thy binders (s,t) env = case (Envir.head_norm env s, Envir.head_norm env t) of
       (Abs(ns,Ts,ts),Abs(nt,Tt,tt)) =>
          let val name = if ns = "" then nt else ns
-         in unif thy ((name,Ts)::binders) (ts,tt) env end
+         in unif thy ((name,Ts)::binders) (ts,tt) (unify_types thy (Ts, Tt) env) end
     | (Abs(ns,Ts,ts),t) => unif thy ((ns,Ts)::binders) (ts,(incr t)$Bound(0)) env
     | (t,Abs(nt,Tt,tt)) => unif thy ((nt,Tt)::binders) ((incr t)$Bound(0),tt) env
     | p => cases thy (binders,env,p)
isabelle