equal
deleted
inserted
replaced
413 in from t end; |
413 in from t end; |
414 |
414 |
415 (*A debugging function: replaces all Vars by dummy Frees for visual inspection |
415 (*A debugging function: replaces all Vars by dummy Frees for visual inspection |
416 of whether they are distinct. Function revert undoes the assignments.*) |
416 of whether they are distinct. Function revert undoes the assignments.*) |
417 fun instVars t = |
417 fun instVars t = |
418 let val name = ref "A" |
418 let val name = ref "a" |
419 val updated = ref [] |
419 val updated = ref [] |
420 fun inst (TConst(a,t)) = inst t |
420 fun inst (TConst(a,t)) = inst t |
421 | inst (Var(v as ref None)) = (updated := v :: (!updated); |
421 | inst (Var(v as ref None)) = (updated := v :: (!updated); |
422 v := Some (Free ("?" ^ !name)); |
422 v := Some (Free ("?" ^ !name)); |
423 name := bump_string (!name)) |
423 name := Symbol.bump_string (!name)) |
424 | inst (Abs(a,t)) = inst t |
424 | inst (Abs(a,t)) = inst t |
425 | inst (f $ u) = (inst f; inst u) |
425 | inst (f $ u) = (inst f; inst u) |
426 | inst _ = () |
426 | inst _ = () |
427 fun revert() = seq (fn v => v:=None) (!updated) |
427 fun revert() = seq (fn v => v:=None) (!updated) |
428 in inst t; revert end; |
428 in inst t; revert end; |