--- a/src/HOL/Auth/Guard/Guard_Public.thy Mon Mar 01 13:42:31 2010 +0100
+++ b/src/HOL/Auth/Guard/Guard_Public.thy Mon Mar 01 16:42:45 2010 +0100
@@ -85,11 +85,10 @@
subsubsection{*greatest nonce used in a trace, 0 if there is no nonce*}
-consts greatest :: "event list => nat"
-
-recdef greatest "measure size"
-"greatest [] = 0"
-"greatest (ev # evs) = max (greatest_msg (msg ev)) (greatest evs)"
+primrec greatest :: "event list => nat"
+where
+ "greatest [] = 0"
+| "greatest (ev # evs) = max (greatest_msg (msg ev)) (greatest evs)"
lemma greatest_is_greatest: "Nonce n:used evs ==> n <= greatest evs"
apply (induct evs, auto simp: initState.simps)