equal
deleted
inserted
replaced
102 * |
102 * |
103 * Types |
103 * Types |
104 * |
104 * |
105 *---------------------------------------------------------------------------*) |
105 *---------------------------------------------------------------------------*) |
106 val mk_prim_vartype = TVar; |
106 val mk_prim_vartype = TVar; |
107 fun mk_vartype s = mk_prim_vartype ((s, 0), HOLogic.typeS); |
107 fun mk_vartype s = mk_prim_vartype ((s, 0), @{sort type}); |
108 |
108 |
109 (* But internally, it's useful *) |
109 (* But internally, it's useful *) |
110 fun dest_vtype (TVar x) = x |
110 fun dest_vtype (TVar x) = x |
111 | dest_vtype _ = raise USYN_ERR "dest_vtype" "not a flexible type variable"; |
111 | dest_vtype _ = raise USYN_ERR "dest_vtype" "not a flexible type variable"; |
112 |
112 |