diff -r 515e5496171c -r 07f775729e90 Nominal/Nominal2.thy
--- a/Nominal/Nominal2.thy	Mon Dec 06 16:35:42 2010 +0000
+++ b/Nominal/Nominal2.thy	Mon Dec 06 17:11:34 2010 +0000
@@ -5,7 +5,6 @@
      ("nominal_dt_rawfuns.ML")
      ("nominal_dt_alpha.ML")
      ("nominal_dt_quot.ML")
-     ("nominal_dt_supp.ML")
 begin
 
 use "nominal_dt_rawperm.ML"
@@ -20,8 +19,6 @@
 use "nominal_dt_quot.ML"
 ML {* open Nominal_Dt_Quot *}
 
-use "nominal_dt_supp.ML"
-ML {* open Nominal_Dt_Supp *}
 
 section{* Interface for nominal_datatype *}