# HG changeset patch
# User berghofe
# Date 1161557325 -7200
# Node ID fe9f43a1e5bdd5b56ceaa139d3e17b4490846fef
# Parent  3cb13b06ad7258d3688596145c8303caa293c456
Added Compile and Height examples.

diff -r 3cb13b06ad72 -r fe9f43a1e5bd 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";