diff -r 5ac9a74d22fd -r 2e174807c891 Nominal/nominal_dt_supp.ML
--- a/Nominal/nominal_dt_supp.ML	Mon Sep 27 09:51:15 2010 -0400
+++ b/Nominal/nominal_dt_supp.ML	Mon Sep 27 12:19:17 2010 -0400
@@ -20,8 +20,6 @@
 structure Nominal_Dt_Supp: NOMINAL_DT_SUPP =
 struct
 
-fun lookup xs x = the (AList.lookup (op=) xs x)
-
 (* supports lemmas for constructors *)
 
 fun mk_supports_goal ctxt qtrm =