diff -r 6927a62c77dc -r 81bf91654e73 src/LCF/ex/Ex3.thy
--- a/src/LCF/ex/Ex3.thy	Sat Sep 03 17:54:07 2005 +0200
+++ b/src/LCF/ex/Ex3.thy	Sat Sep 03 17:54:10 2005 +0200
@@ -1,14 +1,20 @@
 
-(*** Addition with fixpoint of successor ***)
+(* $Id$ *)
+
+header {* Addition with fixpoint of successor *}
 
-Ex3 = LCF +
+theory Ex3
+imports LCF
+begin
 
 consts
-  s	:: "'a => 'a"
-  p	:: "'a => 'a => 'a"
+  s     :: "'a => 'a"
+  p     :: "'a => 'a => 'a"
 
-rules
-  p_strict	"p(UU) = UU"
-  p_s		"p(s(x),y) = s(p(x,y))"
+axioms
+  p_strict:     "p(UU) = UU"
+  p_s:          "p(s(x),y) = s(p(x,y))"
+
+ML {* use_legacy_bindings (the_context ()) *}
 
 end