diff -r 320775fa47ca -r d0961e6d6881 Nominal/nominal_dt_supp.ML
--- a/Nominal/nominal_dt_supp.ML	Mon Sep 27 04:56:28 2010 -0400
+++ b/Nominal/nominal_dt_supp.ML	Mon Sep 27 04:56:49 2010 -0400
@@ -122,13 +122,13 @@
 fun symmetric thms = 
   map (fn thm => thm RS @{thm sym}) thms
 
-val supp_abs_set = @{thms supp_abs(1)[symmetric]}
-val supp_abs_res = @{thms supp_abs(2)[symmetric]}
-val supp_abs_lst = @{thms supp_abs(3)[symmetric]}
+val supp_Abs_set = @{thms supp_Abs(1)[symmetric]}
+val supp_Abs_res = @{thms supp_Abs(2)[symmetric]}
+val supp_Abs_lst = @{thms supp_Abs(3)[symmetric]}
 
-fun mk_supp_abs ctxt (BC (Set, _, _)) = EqSubst.eqsubst_tac ctxt [1] supp_abs_set 
-  | mk_supp_abs ctxt (BC (Res, _, _)) = EqSubst.eqsubst_tac ctxt [1] supp_abs_res
-  | mk_supp_abs ctxt (BC (Lst, _, _)) = EqSubst.eqsubst_tac ctxt [1] supp_abs_lst
+fun mk_supp_abs ctxt (BC (Set, _, _)) = EqSubst.eqsubst_tac ctxt [1] supp_Abs_set 
+  | mk_supp_abs ctxt (BC (Res, _, _)) = EqSubst.eqsubst_tac ctxt [1] supp_Abs_res
+  | mk_supp_abs ctxt (BC (Lst, _, _)) = EqSubst.eqsubst_tac ctxt [1] supp_Abs_lst
 
 fun mk_supp_abs_tac ctxt [] = []
   | mk_supp_abs_tac ctxt (BC (_, [], _)::xs) = mk_supp_abs_tac ctxt xs
@@ -139,8 +139,8 @@
   |> fastype_of
   |> body_type
   |> (fn ty => case ty of
-        @{typ "atom set"}  => simp_tac (add_ss supp_abs_set)
-      | @{typ "atom list"} => simp_tac (add_ss supp_abs_lst)
+        @{typ "atom set"}  => simp_tac (add_ss supp_Abs_set)
+      | @{typ "atom list"} => simp_tac (add_ss supp_Abs_lst)
       | _ => raise TERM ("mk_bn_supp_abs_tac", [trm]))