--- 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")
],