equal
deleted
inserted
replaced
101 (** raw typs/terms to pretyps/preterms **) |
101 (** raw typs/terms to pretyps/preterms **) |
102 |
102 |
103 (* pretyp(s)_of *) |
103 (* pretyp(s)_of *) |
104 |
104 |
105 fun anyT S = TFree ("'_dummy_", S); |
105 fun anyT S = TFree ("'_dummy_", S); |
106 val logicT = anyT logicS; |
106 val logicT = anyT []; |
107 |
107 |
108 (*indicate polymorphic Vars*) |
108 (*indicate polymorphic Vars*) |
109 fun polymorphicT T = Type ("_polymorphic_", [T]); |
109 fun polymorphicT T = Type ("_polymorphic_", [T]); |
110 |
110 |
111 fun pretyp_of is_param (params, typ) = |
111 fun pretyp_of is_param (params, typ) = |