diff -r 0467dd0d66ff -r 9df44a4f1bf7 src/HOL/Gfp.thy
--- a/src/HOL/Gfp.thy	Thu May 18 11:40:57 2000 +0200
+++ b/src/HOL/Gfp.thy	Thu May 18 11:43:57 2000 +0200
@@ -8,12 +8,8 @@
 
 Gfp = Lfp +
 
-global
-
 constdefs
   gfp :: ['a set=>'a set] => 'a set
   "gfp(f) == Union({u. u <= f(u)})"    (*greatest fixed point*)
 
-local
-
 end