diff -r 84afb941df53 -r d1038e67923a Nominal/Nominal2.thy
--- a/Nominal/Nominal2.thy	Mon Jul 18 10:50:21 2011 +0100
+++ b/Nominal/Nominal2.thy	Mon Jul 18 17:40:13 2011 +0100
@@ -10,6 +10,7 @@
      ("nominal_function_core.ML")
      ("nominal_mutual.ML")
      ("nominal_function.ML")
+     ("nominal_termination.ML")
      ("nominal_dt_data.ML")
 begin
 
@@ -44,6 +45,7 @@
 use "nominal_function_core.ML"
 use "nominal_mutual.ML"
 use "nominal_function.ML"
+use "nominal_termination.ML"
 
 ML {*
 val eqvt_attr = Attrib.internal (K Nominal_ThmDecls.eqvt_add)