--- 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