--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML Fri Aug 30 11:27:23 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML Fri Aug 30 11:37:22 2013 +0200
@@ -47,7 +47,7 @@
};
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
@@ -674,7 +674,7 @@
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
@@ -741,4 +741,3 @@
uncurry add_primcorec_cmd);
end;
-