equal
deleted
inserted
replaced
101 val (t, tvars) = |
101 val (t, tvars) = |
102 (case ty of |
102 (case ty of |
103 Type (t, tys) => (t, map dest_varT tys handle TYPE _ => err ()) |
103 Type (t, tys) => (t, map dest_varT tys handle TYPE _ => err ()) |
104 | _ => err ()); |
104 | _ => err ()); |
105 val ss = |
105 val ss = |
106 if null (gen_duplicates eq_fst tvars) |
106 if null (gen_duplicates (eq_fst (op =)) tvars) |
107 then map snd tvars else err (); |
107 then map snd tvars else err (); |
108 in (t, ss, c) end; |
108 in (t, ss, c) end; |
109 |
109 |
110 |
110 |
111 |
111 |