--- a/ProgTutorial/Essential.thy	Thu Feb 11 10:44:50 2010 +0100
+++ b/ProgTutorial/Essential.thy	Sun Mar 07 21:15:05 2010 +0100
@@ -39,7 +39,7 @@
   @{ML_response [display,gray] 
 "@{term \"(a::nat) + b = c\"}" 
 "Const (\"op =\", \<dots>) $ 
-  (Const (\"Algebras.plus_class.plus\", \<dots>) $ \<dots> $ \<dots>) $ \<dots>"}
+  (Const (\"Groups.plus_class.plus\", \<dots>) $ \<dots> $ \<dots>) $ \<dots>"}
 
   constructs the term @{term "(a::nat) + b = c"}. The resulting term is printed using 
   the internal representation corresponding to the datatype @{ML_type_ind "term"}, 
@@ -533,8 +533,8 @@
   \mbox{@{text "(op *)"}}:
 
   @{ML_response [display,gray] "(@{term \"0::nat\"}, @{term \"(op *)\"})" 
- "(Const (\"Algebras.zero_class.zero\", \<dots>), 
- Const (\"Algebras.times_class.times\", \<dots>))"}
+ "(Const (\"Groups.zero_class.zero\", \<dots>), 
+ Const (\"Groups.times_class.times\", \<dots>))"}
 
   While you could use the complete name, for example 
   @{ML "Const (\"List.list.Nil\", some_type)" for some_type}, for referring to or
@@ -770,6 +770,9 @@
   assumption about the sorts, they are incomparable.
 *}
 
+class s1
+class s2 
+
 ML{*val (tyenv, index) = let
   val ty1 = @{typ_pat "?'a::s1"}
   val ty2 = @{typ_pat "?'b::s2"}
@@ -1639,26 +1642,26 @@
   stated using object logic connectives, while theorems using the connectives 
   from the meta logic are more convenient for reasoning. Therefore there are
   some build in functions which help with these transformations. The function 
-  @{ML_ind rulify in ObjectLogic} 
+  @{ML_ind rulify in Object_Logic} 
   replaces all object connectives by equivalents in the meta logic. For example
 
   @{ML_response_fake [display, gray]
-  "ObjectLogic.rulify @{thm foo_test2}"
+  "Object_Logic.rulify @{thm foo_test2}"
   "\<lbrakk>?A; ?B\<rbrakk> \<Longrightarrow> ?C"}
 
   The transformation in the other direction can be achieved with function
-  @{ML_ind atomize in ObjectLogic} and the following code.
+  @{ML_ind atomize in Object_Logic} and the following code.
 
   @{ML_response_fake [display,gray]
   "let
   val thm = @{thm foo_test1}
-  val meta_eq = ObjectLogic.atomize (cprop_of thm)
+  val meta_eq = Object_Logic.atomize (cprop_of thm)
 in
   MetaSimplifier.rewrite_rule [meta_eq] thm
 end"
   "?A \<longrightarrow> ?B \<longrightarrow> ?C"}
 
-  In this code the function @{ML atomize in ObjectLogic} produces 
+  In this code the function @{ML atomize in Object_Logic} produces 
   a meta-equation between the given theorem and the theorem transformed
   into the object logic. The result is the theorem with object logic 
   connectives. However, in order to completely transform a theorem
@@ -1676,7 +1679,7 @@
 ML{*fun atomize_thm thm =
 let
   val thm' = forall_intr_vars thm
-  val thm'' = ObjectLogic.atomize (cprop_of thm')
+  val thm'' = Object_Logic.atomize (cprop_of thm')
 in
   MetaSimplifier.rewrite_rule [thm''] thm'
 end*}
@@ -1688,8 +1691,6 @@
   "atomize_thm @{thm list.induct}"
   "\<forall>P list. P [] \<longrightarrow> (\<forall>a list. P list \<longrightarrow> P (a # list)) \<longrightarrow> P list"}
 
-  \footnote{\bf FIXME: say someting about @{ML_ind standard in Drule}.}
-
   Theorems can also be produced from terms by giving an explicit proof. 
   One way to achieve this is by using the function @{ML_ind prove in Goal}
   in the structure @{ML_struct Goal}. For example below we use this function