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