--- a/ProgTutorial/Essential.thy	Sun Nov 22 03:13:29 2009 +0100
+++ b/ProgTutorial/Essential.thy	Sun Nov 22 15:27:10 2009 +0100
@@ -6,7 +6,7 @@
 setup{*
 open_file_with_prelude 
   "Essential_Code.thy"
-  ["theory General", "imports Base FirstSteps", "begin"]
+  ["theory Essential", "imports Base FirstSteps", "begin"]
 *}
 (*>*)
 
@@ -1644,9 +1644,6 @@
   "Skip_Proof.make_thm @{theory} @{prop \"True = False\"}"
   "True = False"}
 
-  The function @{ML make_thm in Skip_Proof} however only works if 
-  the ``quick-and-dirty'' mode is switched on. 
-
   Theorems also contain auxiliary data, such as the name of the theorem, its
   kind, the names for cases and so on. This data is stored in a string-string
   list and can be retrieved with the function @{ML_ind get_tags in