equal
deleted
inserted
replaced
309 fun mkvar T = |
309 fun mkvar T = |
310 Mfix ("_", varT --> change_name T "_A", "", [], max_pri); |
310 Mfix ("_", varT --> change_name T "_A", "", [], max_pri); |
311 |
311 |
312 fun constrain T = |
312 fun constrain T = |
313 Mfix ("_::_", [T, typeT] ---> change_name T "_A", constrainC, |
313 Mfix ("_::_", [T, typeT] ---> change_name T "_A", constrainC, |
314 [max_pri, 0], max_pri - 1) |
314 [4, 0], 3) |
315 |
315 |
316 fun unhide T = |
316 fun unhide T = |
317 if T <> logicT then |
317 if T <> logicT then |
318 [Mfix ("_", change_name T "_H" --> T, "", [0], 0), |
318 [Mfix ("_", change_name T "_H" --> T, "", [0], 0), |
319 Mfix ("_", change_name T "_A" --> T, "", [0], 0)] |
319 Mfix ("_", change_name T "_A" --> T, "", [0], 0)] |