src/HOL/BNF/Tools/bnf_wrap.ML

 val cong_attrs = @{attributes [cong]};
 val iff_attrs = @{attributes [iff]};
 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)));
 
 fun mk_half_pairss' _ ([], []) = []

 
     val uv_eq = mk_Trueprop_eq (u, v);
 
     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
           NONE => nth exist_xs_u_eq_ctrs (k - 1)