equal
deleted
inserted
replaced
53 end |
53 end |
54 |
54 |
55 fun proper_match ps env = |
55 fun proper_match ps env = |
56 forall (forall (not o typ_has_tvars o Envir.subst_type env) o snd) ps |
56 forall (forall (not o typ_has_tvars o Envir.subst_type env) o snd) ps |
57 |
57 |
58 val eq_tab = gen_eq_set (op =) o pairself Vartab.dest |
58 val eq_tab = eq_set (op =) o pairself Vartab.dest |
59 |
59 |
60 fun specialize thy cs is ((r, ps), ces) (ts, ns) = |
60 fun specialize thy cs is ((r, ps), ces) (ts, ns) = |
61 let |
61 let |
62 val ps' = filter (AList.defined (op =) is o fst) ps |
62 val ps' = filter (AList.defined (op =) is o fst) ps |
63 |
63 |