src/HOL/BNF/Tools/bnf_def.ML

   let
     val Type (_, Ts) = T_of_bnf bnf;
     val lives = lives_of_bnf bnf;
     val deads = deads_of_bnf bnf;
   in
-    mk_permute (op =) (deads @ lives) Ts (replicate (length deads) dead_x @ xs)
+    permute_like (op =) (deads @ lives) Ts (replicate (length deads) dead_x @ xs)
   end;
 
 (*terms*)
 val map_of_bnf = #map o rep_bnf;
 val sets_of_bnf = #sets o rep_bnf;