diff -r 7330e4eefbd7 -r 426d5781bb25 src/HOL/Auth/Kerberos_BAN_Gets.thy
--- a/src/HOL/Auth/Kerberos_BAN_Gets.thy	Wed May 12 15:25:58 2010 +0200
+++ b/src/HOL/Auth/Kerberos_BAN_Gets.thy	Wed May 12 16:44:49 2010 +0200
@@ -52,15 +52,15 @@
   "expiredA T evs == authlife + T < CT evs"
 
 
-constdefs
+definition
  (* Yields the subtrace of a given trace from its beginning to a given event *)
   before :: "[event, event list] => event list" ("before _ on _")
-   "before ev on evs ==  takeWhile (% z. z ~= ev) (rev evs)"
+  where "before ev on evs = takeWhile (% z. z ~= ev) (rev evs)"
 
+definition
  (* States than an event really appears only once on a trace *)
   Unique :: "[event, event list] => bool" ("Unique _ on _")
-   "Unique ev on evs == 
-      ev \<notin> set (tl (dropWhile (% z. z \<noteq> ev) evs))"
+  where "Unique ev on evs = (ev \<notin> set (tl (dropWhile (% z. z \<noteq> ev) evs)))"
 
 
 inductive_set bankerb_gets :: "event list set"