(*Makes parameters in a goal have distinctive names (not guaranteed unique!)

 (*Makes parameters in a goal have distinctive names (not guaranteed unique!)

   A name clash could cause the printer to rename bound vars;

   A name clash could cause the printer to rename bound vars;

     then res_inst_tac would not work properly.*)

     then res_inst_tac would not work properly.*)

 fun rename_vars (a, []) = []

 fun rename_vars (a, []) = []

   | rename_vars (a, (_,T)::vars) =

   | rename_vars (a, (_,T)::vars) =

 (*Move all parameters to the front of the subgoal, renaming them apart;

 (*Move all parameters to the front of the subgoal, renaming them apart;

   if n>0 then deletes assumption n. *)

   if n>0 then deletes assumption n. *)

 fun flatten_params n A =

 fun flatten_params n A =

     let val params = strip_params A;

     let val params = strip_params A;