diff -r 4e68398cdc06 -r 4a213aaca3d9 src/LCF/ex.ML
--- a/src/LCF/ex.ML	Tue Dec 21 16:38:45 1993 +0100
+++ b/src/LCF/ex.ML	Tue Dec 21 16:40:01 1993 +0100
@@ -14,7 +14,7 @@
 (***  Section 10.4  ***)
 
 val ex_thy = extend_theory thy "Ex 10.4"
-([], [], [], [],
+([], [], [], [], [],
  [(["P"], "'a => tr"),
   (["G","H"], "'a => 'a"),
   (["K"], "('a => 'a) => ('a => 'a)")
@@ -56,7 +56,7 @@
 (***  Example 3.8  ***)
 
 val ex_thy = extend_theory thy "Ex 3.8"
-([], [], [], [],
+([], [], [], [], [],
  [(["P"], "'a => tr"),
   (["F","G"], "'a => 'a"),
   (["H"], "'a => 'b => 'b"),
@@ -86,7 +86,7 @@
 (*** Addition with fixpoint of successor ***)
 
 val ex_thy = extend_theory thy "fix ex"
-([], [], [], [],
+([], [], [], [], [],
  [(["s"], "'a => 'a"),
   (["p"], "'a => 'a => 'a")
  ],