diff -r 7330e4eefbd7 -r 426d5781bb25 src/HOL/Auth/NS_Shared.thy
--- a/src/HOL/Auth/NS_Shared.thy	Wed May 12 15:25:58 2010 +0200
+++ b/src/HOL/Auth/NS_Shared.thy	Wed May 12 16:44:49 2010 +0200
@@ -14,15 +14,14 @@
   Proc. Royal Soc. 426
 *}
 
-constdefs
-
+definition
  (* A is the true creator of X if she has sent X and X never appeared on
     the trace before this event. Recall that traces grow from head. *)
   Issues :: "[agent, agent, msg, event list] => bool"
-             ("_ Issues _ with _ on _")
-   "A Issues B with X on evs ==
-      \<exists>Y. Says A B Y \<in> set evs & X \<in> parts {Y} &
-      X \<notin> parts (spies (takeWhile (% z. z  \<noteq> Says A B Y) (rev evs)))"
+             ("_ Issues _ with _ on _") where
+   "A Issues B with X on evs =
+      (\<exists>Y. Says A B Y \<in> set evs & X \<in> parts {Y} &
+        X \<notin> parts (spies (takeWhile (% z. z  \<noteq> Says A B Y) (rev evs))))"
 
 
 inductive_set ns_shared :: "event list set"