1.1 --- a/src/Tools/subtyping.ML	Wed Sep 28 13:52:14 2011 +0200
     1.2 +++ b/src/Tools/subtyping.ML	Thu Sep 29 09:37:59 2011 +0200
     1.3 @@ -628,7 +628,7 @@
     1.4                  NONE => raise COERCION_GEN_ERROR (err ++> quote (Syntax.string_of_typ ctxt T1) ^
     1.5                    " is not a subtype of " ^ quote (Syntax.string_of_typ ctxt T2))
     1.6                | SOME (co, _) => co)
     1.7 -      | ((Type (a, Ts)), (Type (b, Us))) =>
     1.8 +      | (T1 as Type (a, Ts), T2 as Type (b, Us)) =>
     1.9              if a <> b
    1.10              then
    1.11                (case Symreltab.lookup (coes_of ctxt) (a, b) of
    1.12 @@ -656,8 +656,11 @@
    1.13                    | ts_of (Type ("fun", [x1, x2]) :: xs) = x1 :: x2 :: (ts_of xs);
    1.14                in
    1.15                  (case Symtab.lookup (tmaps_of ctxt) a of
    1.16 -                  NONE => raise COERCION_GEN_ERROR
    1.17 -                    (err ++> "No map function for " ^ quote a ^ " known")
    1.18 +                  NONE =>
    1.19 +                    if Type.could_unify (T1, T2)
    1.20 +                    then Abs (Name.uu, T1, Bound 0)
    1.21 +                    else raise COERCION_GEN_ERROR
    1.22 +                      (err ++> "No map function for " ^ quote a ^ " known")
    1.23                  | SOME tmap =>
    1.24                      let
    1.25                        val used_coes = map_filter sub_co ((snd tmap) ~~ (Ts ~~ Us));