684 | fish_parm _ NONE = NONE; |
684 | fish_parm _ NONE = NONE; |
685 fun fillup_parm _ (_, SOME v) = v |
685 fun fillup_parm _ (_, SOME v) = v |
686 | fillup_parm x (i, NONE) = x ^ string_of_int i; |
686 | fillup_parm x (i, NONE) = x ^ string_of_int i; |
687 fun fish_parms vars eqs = |
687 fun fish_parms vars eqs = |
688 let |
688 let |
689 val raw_fished = fold (map2 fish_parm) eqs (replicate (length (hd eqs)) NONE); |
689 val fished1 = fold (map2 fish_parm) eqs (replicate (length (hd eqs)) NONE); |
690 val x = Name.variant (map_filter I raw_fished) "x"; |
690 val x = Name.variant (map_filter I fished1) "x"; |
691 val fished = map_index (fillup_parm x) raw_fished; |
691 val fished2 = map_index (fillup_parm x) fished1; |
692 val vars' = CodeName.intro_vars fished vars; |
692 val (fished3, _) = Name.variants fished2 Name.context; |
693 in map (CodeName.lookup_var vars') fished end; |
693 val vars' = CodeName.intro_vars fished3 vars; |
|
694 in map (CodeName.lookup_var vars') fished3 end; |
694 fun pr_eq (ts, t) = |
695 fun pr_eq (ts, t) = |
695 let |
696 let |
696 val consts = map_filter |
697 val consts = map_filter |
697 (fn c => if (is_some o const_syntax) c |
698 (fn c => if (is_some o const_syntax) c |
698 then NONE else (SOME o NameSpace.base o deresolv) c) |
699 then NONE else (SOME o NameSpace.base o deresolv) c) |