equal
deleted
inserted
replaced
589 |
589 |
590 |
590 |
591 |
591 |
592 local fun dest_pair M = let val {fst,snd} = S.dest_pair M in (fst,snd) end |
592 local fun dest_pair M = let val {fst,snd} = S.dest_pair M in (fst,snd) end |
593 fun mk_fst tm = |
593 fun mk_fst tm = |
594 let val ty as Type("*", [fty,sty]) = type_of tm |
594 let val ty as Type("Product_Type.*", [fty,sty]) = type_of tm |
595 in Const ("fst", ty --> fty) $ tm end |
595 in Const ("Product_Type.fst", ty --> fty) $ tm end |
596 fun mk_snd tm = |
596 fun mk_snd tm = |
597 let val ty as Type("*", [fty,sty]) = type_of tm |
597 let val ty as Type("Product_Type.*", [fty,sty]) = type_of tm |
598 in Const ("snd", ty --> sty) $ tm end |
598 in Const ("Product_Type.snd", ty --> sty) $ tm end |
599 in |
599 in |
600 fun XFILL tych x vstruct = |
600 fun XFILL tych x vstruct = |
601 let fun traverse p xocc L = |
601 let fun traverse p xocc L = |
602 if (is_Free p) |
602 if (is_Free p) |
603 then tych xocc::L |
603 then tych xocc::L |