77 val distinct_typevars = map TFree tvars; |
77 val distinct_typevars = map TFree tvars; |
78 fun rm_sorts (TFree(s,_)) = TFree(s,[]) |
78 fun rm_sorts (TFree(s,_)) = TFree(s,[]) |
79 | rm_sorts (Type(s,ts)) = Type(s,remove_sorts ts) |
79 | rm_sorts (Type(s,ts)) = Type(s,remove_sorts ts) |
80 | rm_sorts (TVar(s,_)) = TVar(s,[]) |
80 | rm_sorts (TVar(s,_)) = TVar(s,[]) |
81 and remove_sorts l = map rm_sorts l; |
81 and remove_sorts l = map rm_sorts l; |
82 val indirect_ok = ["*","Cfun.->","Ssum.++","Sprod.**","Up.u"] |
82 val indirect_ok = |
|
83 [@{type_name "*"}, @{type_name cfun}, @{type_name ssum}, |
|
84 @{type_name sprod}, @{type_name u}]; |
83 fun analyse indirect (TFree(v,s)) = |
85 fun analyse indirect (TFree(v,s)) = |
84 (case AList.lookup (op =) tvars v of |
86 (case AList.lookup (op =) tvars v of |
85 NONE => error ("Free type variable " ^ quote v ^ " on rhs.") |
87 NONE => error ("Free type variable " ^ quote v ^ " on rhs.") |
86 | SOME sort => if eq_set (op =) (s, defaultS) orelse |
88 | SOME sort => if eq_set (op =) (s, defaultS) orelse |
87 eq_set (op =) (s, sort) |
89 eq_set (op =) (s, sort) |