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.
collapse map functions with identity subcoercions to identities;
authortraytel
Tue, 28 Jun 2011 10:52:15 +0200
changeset 43591 d4cbd6feffdf
parent 43590 0940a64beca2
child 43592 e67d104c0c50
child 43607 119767e1ccb4
collapse map functions with identity subcoercions to identities;
src/Tools/subtyping.ML file | annotate | diff | comparison | revisions 
--- a/src/Tools/subtyping.ML	Tue Jun 28 21:06:59 2011 +0200
+++ b/src/Tools/subtyping.ML	Tue Jun 28 10:52:15 2011 +0200
@@ -84,6 +84,7 @@
 val is_freeT = fn (TFree _) => true | _ => false;
 val is_fixedvarT = fn (TVar (xi, _)) => not (Type_Infer.is_param xi) | _ => false;
 val is_funtype = fn (Type ("fun", [_, _])) => true | _ => false;
+val is_identity = fn (Abs (_, _, Bound 0)) => true | _ => false;
 
 
 (* unification *)
@@ -614,7 +615,9 @@
                 let
                   val used_coes = map_filter sub_co ((snd tmap) ~~ (Ts ~~ Us));
                 in
-                  Term.list_comb
+                  if null (filter (not o is_identity) used_coes)
+                  then Abs (Name.uu, Type (a, Ts), Bound 0)
+                  else Term.list_comb
                     (inst (fst tmap) (ts_of (map fastype_of used_coes)), used_coes)
                 end)
           end
isabelle