src/HOL/Nominal/Examples/ROOT.ML

--- a/src/HOL/Nominal/Examples/ROOT.ML	Mon Oct 23 00:47:25 2006 +0200
+++ b/src/HOL/Nominal/Examples/ROOT.ML	Mon Oct 23 00:48:45 2006 +0200
@@ -7,7 +7,9 @@
 
 use_thy "CR";
 use_thy "Class";
-setmp quick_and_dirty true use_thy "Fsub"; (* FIXME *)
+use_thy "Compile";
+use_thy "Fsub";
+use_thy "Height";
 use_thy "Lambda_mu";
 use_thy "Recursion";
 use_thy "SN";