src/FOLP/ex/ROOT.ML

--- a/src/FOLP/ex/ROOT.ML	Sat Sep 17 20:49:14 2005 +0200
+++ b/src/FOLP/ex/ROOT.ML	Sun Sep 18 14:25:48 2005 +0200
@@ -1,9 +1,9 @@
-(*  Title:      FOLP/ex/ROOT
+(*  Title:      FOLP/ex/ROOT.ML
     ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1992  University of Cambridge
 
-Executes all examples for First-Order Logic. 
+Examples for First-Order Logic. 
 *)
 
 time_use     "intro.ML";
@@ -13,7 +13,7 @@
 writeln"\n** Intuitionistic examples **\n";
 time_use     "int.ML";
 
-val thy = IFOLP.thy  and  tac = IntPr.fast_tac 1;
+val thy = theory "IFOLP"  and  tac = IntPr.fast_tac 1;
 time_use     "prop.ML";
 time_use     "quant.ML";
 
@@ -21,6 +21,6 @@
 time_use     "cla.ML";
 time_use_thy "If";
 
-val thy = FOLP.thy  and  tac = Cla.fast_tac FOLP_cs 1;
+val thy = theory "FOLP"  and  tac = Cla.fast_tac FOLP_cs 1;
 time_use     "prop.ML";
 time_use     "quant.ML";