src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML

   rhs_term: term,
   user_eqn: term
 };
 
 fun permute_args n t = list_comb (t, map Bound (0 :: (n downto 1)))
-  |> fold (K (fn u => Abs ("", dummyT, u))) (0 upto n);
+  |> fold (K (fn u => Abs (Name.uu, dummyT, u))) (0 upto n);
 
 fun dissect_eqn lthy fun_names eqn' =
   let
     val eqn = subst_bounds (strip_qnt_vars @{const_name all} eqn' |> map Free |> rev,
         strip_qnt_body @{const_name all} eqn') |> HOLogic.dest_Trueprop

             Abs (v, T, u)) abs_vars t);
 
     fun currys Ts t = if length Ts <= 1 then t else
       t $ foldr1 (fn (u, v) => HOLogic.pair_const dummyT dummyT $ u $ v)
         (length Ts - 1 downto 0 |> map Bound)
-      |> fold_rev (fn T => fn u => Abs ("", T, u)) Ts;
+      |> fold_rev (fn T => fn u => Abs (Name.uu, T, u)) Ts;
   in
     map (list_comb o rpair corec_args) corecs
     |> map2 (fn Ts => fn t => if length Ts = 0 then t $ HOLogic.unit else t) arg_Tss
     |> map2 currys arg_Tss
     |> Syntax.check_terms lthy

   "define primitive corecursive functions"
   (Parse.opt_keyword "sequential" -- (Parse.fixes -- Parse_Spec.where_alt_specs) >>
     uncurry add_primcorec_cmd);
 
 end;
-