src/HOL/Nominal/Examples/ROOT.ML
changeset 33615 261abc2e3155
parent 32635 37e32f8aa696
child 33773 ccef2e6d8c21
--- a/src/HOL/Nominal/Examples/ROOT.ML	Wed Nov 11 09:02:37 2009 +0100
+++ b/src/HOL/Nominal/Examples/ROOT.ML	Wed Nov 11 14:15:11 2009 +0100
@@ -1,4 +1,3 @@
+use_thys ["Nominal_Examples"];
 
-use_thy "Nominal_Examples";
-
-setmp_noncritical quick_and_dirty true use_thy "VC_Condition"; (*FIXME*)
+setmp_noncritical quick_and_dirty true use_thys ["VC_Condition"]; (*FIXME*)