# HG changeset patch # User blanchet # Date 1346830291 -7200 # Node ID e36ce78add78b8a7bb86902e5679d722d476b752 # Parent 53f954510a8cfeb07305b3e7c3dfb3b8ea3dd608 use empty binding rather than "*" for default diff -r 53f954510a8c -r e36ce78add78 src/HOL/Codatatype/Tools/bnf_wrap.ML --- a/src/HOL/Codatatype/Tools/bnf_wrap.ML Wed Sep 05 08:32:59 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_wrap.ML Wed Sep 05 09:31:31 2012 +0200 @@ -40,7 +40,7 @@ val split_asmN = "split_asm"; val weak_case_cong_thmsN = "weak_case_cong"; -val no_binder = @{binding "*"}; +val no_binder = @{binding ""}; val fallback_binder = @{binding _}; fun pad_list x n xs = xs @ replicate (n - length xs) x;