equal
deleted
inserted
replaced
819 |
819 |
820 |
820 |
821 (* user parameters *) |
821 (* user parameters *) |
822 |
822 |
823 fun is_param (x, _) = size x > 0 andalso ord x = ord "?"; |
823 fun is_param (x, _) = size x > 0 andalso ord x = ord "?"; |
824 fun param used (x, S) = TVar (("?" ^ variant used x, 0), S); |
824 fun param used (x, S) = TVar ((variant used ("?" ^ x), 0), S); |
825 |
825 |
826 |
826 |
827 (* decode_types *) |
827 (* decode_types *) |
828 |
828 |
829 (*transform parse tree into raw term*) |
829 (*transform parse tree into raw term*) |