equal
deleted
inserted
replaced
28 val pairs = ref ([] : (term*term) list) |
28 val pairs = ref ([] : (term*term) list) |
29 fun insert t = |
29 fun insert t = |
30 let val T = fastype_of t |
30 let val T = fastype_of t |
31 val v = Unify.combound (Var ((!vname,0), Us--->T), |
31 val v = Unify.combound (Var ((!vname,0), Us--->T), |
32 0, nPar) |
32 0, nPar) |
33 in vname := bump_string (!vname); |
33 in vname := Symbol.bump_string (!vname); |
34 pairs := (t, v) :: !pairs; |
34 pairs := (t, v) :: !pairs; |
35 v |
35 v |
36 end; |
36 end; |
37 fun replace t = |
37 fun replace t = |
38 case t of |
38 case t of |