diff -r b5ff7393642d -r 51f1f4ba18f3 src/HOL/BNF/Tools/bnf_wrap.ML
--- a/src/HOL/BNF/Tools/bnf_wrap.ML	Tue Apr 23 16:41:59 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_wrap.ML	Tue Apr 23 16:49:14 2013 +0200
@@ -65,9 +65,6 @@
 val safe_elim_attrs = @{attributes [elim!]};
 val simp_attrs = @{attributes [simp]};
 
-val unique_disc_no_def = TrueI; (*arbitrary marker*)
-val alternate_disc_no_def = FalseE; (*arbitrary marker*)
-
 fun pad_list x n xs = xs @ replicate (n - length xs) x;
 
 fun unflat_lookup eq ys zs = map (map (fn x => nth zs (find_index (curry eq x) ys)));
@@ -219,6 +216,9 @@
     val exist_xs_u_eq_ctrs =
       map2 (fn xctr => fn xs => list_exists_free xs (HOLogic.mk_eq (u, xctr))) xctrs xss;
 
+    val unique_disc_no_def = TrueI; (*arbitrary marker*)
+    val alternate_disc_no_def = FalseE; (*arbitrary marker*)
+
     fun alternate_disc_lhs get_udisc k =
       HOLogic.mk_not
         (case nth disc_bindings (k - 1) of