# HG changeset patch
# User wenzelm
# Date 1181737314 -7200
# Node ID ed60e560048dc5239eac92cb4f374f3869f41ea8
# Parent  513a8ee192f13929b36a0f8cdfd49f2597cbe08f
reactivated theory Class;

diff -r 513a8ee192f1 -r ed60e560048d src/HOL/Nominal/Examples/ROOT.ML
--- a/src/HOL/Nominal/Examples/ROOT.ML	Wed Jun 13 12:22:02 2007 +0200
+++ b/src/HOL/Nominal/Examples/ROOT.ML	Wed Jun 13 14:21:54 2007 +0200
@@ -5,9 +5,9 @@
 Various examples involving nominal datatypes.
 *)
 
-(*use_thy "Class";*)
 use_thy "CR";
 use_thy "CR_Takahashi";
+use_thy "Class";
 use_thy "Compile";
 use_thy "Fsub";
 use_thy "Height";