diff -r be6538c7b41d -r bdd411caf5eb ProgTutorial/General.thy
--- a/ProgTutorial/General.thy	Sun Oct 25 16:12:05 2009 +0100
+++ b/ProgTutorial/General.thy	Mon Oct 26 00:00:26 2009 +0100
@@ -1713,8 +1713,9 @@
 fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar"}
 
   Here the layout of @{ML test_str} is much more pleasing to the 
-  eye. The @{ML "0"} in @{ML_ind  blk in Pretty} stands for no indentation
-  of the printed string. You can increase the indentation and obtain
+  eye. The @{ML "0"} in @{ML_ind  blk in Pretty} stands for no hanging 
+  indentation of the printed string. You can increase the indentation 
+  and obtain
   
 @{ML_response_fake [display,gray]
 "let
@@ -1958,6 +1959,9 @@
 
 section {* Managing Name Spaces (TBD) *}
 
+ML {* Sign.intern_type @{theory} "list" *}
+ML {* Sign.intern_const @{theory} "prod_fun" *}
+
 section {* Summary *}
 
 text {*