--- a/src/HOL/IOA/NTP/Correctness.thy	Mon Mar 11 19:42:55 1996 +0100
+++ b/src/HOL/IOA/NTP/Correctness.thy	Mon Mar 11 23:59:22 1996 +0100
@@ -8,14 +8,10 @@
 
 Correctness = Solve + Impl + Spec +
 
-consts
-
-hom :: 'm impl_state => 'm list
+constdefs
 
-defs
-
-hom_def 
-"hom(s) == rq(rec(s)) @ (if rbit(rec s) = sbit(sen s) then sq(sen s) 
-                        else ttl(sq(sen s)))"
+  hom :: 'm impl_state => 'm list
+  "hom(s) == rq(rec(s)) @ (if rbit(rec s) = sbit(sen s) then sq(sen s) 
+                          else ttl(sq(sen s)))"
 
 end