diff -r 39d0cc787d47 -r 548901d05a0e src/HOLCF/Cont.ML
--- a/src/HOLCF/Cont.ML	Tue May 23 12:44:03 2000 +0200
+++ b/src/HOLCF/Cont.ML	Tue May 23 18:06:22 2000 +0200
@@ -3,11 +3,9 @@
     Author:     Franz Regensburger
     Copyright   1993 Technische Universitaet Muenchen
 
-Lemmas for Cont.thy 
+Results about continuity and monotonicity
 *)
 
-open Cont;
-
 (* ------------------------------------------------------------------------ *)
 (* access to definition                                                     *)
 (* ------------------------------------------------------------------------ *)
@@ -121,7 +119,7 @@
 (* ------------------------------------------------------------------------ *)
 
 qed_goal "binchain_cont" thy
-"[| cont(f); x << y |]  ==> range(%i. f(if i = 0 then x else y)) <<| f(y)"
+"[| cont(f); x << y |]  ==> range(%i::nat. f(if i = 0 then x else y)) <<| f(y)"
 (fn prems => 
         [
         (cut_facts_tac prems 1),