# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1258674860 -3600
# Node ID ccef2e6d8c218216b3e0d2e3c33bd89749a010a9
# Parent  b6a1feca2ac207ed01cfe709bdd4d36026203289
removed fixme - quick-and-dirty flag is appropriate

diff -r b6a1feca2ac2 -r ccef2e6d8c21 src/HOL/Nominal/Examples/ROOT.ML
--- a/src/HOL/Nominal/Examples/ROOT.ML	Fri Nov 20 00:20:32 2009 +0100
+++ b/src/HOL/Nominal/Examples/ROOT.ML	Fri Nov 20 00:54:20 2009 +0100
@@ -1,3 +1,3 @@
 use_thys ["Nominal_Examples"];
 
-setmp_noncritical quick_and_dirty true use_thys ["VC_Condition"]; (*FIXME*)
+setmp_noncritical quick_and_dirty true use_thys ["VC_Condition"];