--- a/src/HOL/ex/Acc.thy	Mon Mar 11 19:42:55 1996 +0100
+++ b/src/HOL/ex/Acc.thy	Mon Mar 11 23:59:22 1996 +0100
@@ -11,13 +11,13 @@
 
 Acc = WF + 
 
+constdefs
+  pred :: "['b, ('a * 'b)set] => 'a set"        (*Set of predecessors*)
+  "pred x r == {y. (y,x):r}"
+
 consts
-  pred :: "['b, ('a * 'b)set] => 'a set"        (*Set of predecessors*)
   acc  :: "('a * 'a)set => 'a set"              (*Accessible part*)
 
-defs
-  pred_def  "pred x r == {y. (y,x):r}"
-
 inductive "acc(r)"
   intrs
     pred    "pred a r: Pow(acc(r)) ==> a: acc(r)"