# HG changeset patch
# User haftmann
# Date 1201767361 -3600
# Node ID ecbfe264569446a2ea39dabf7834356eac352540
# Parent  9b5b4bd44f7adb764abe38faf3119ced9b7aa1b3
avoiding dynamic simpset lookup

diff -r 9b5b4bd44f7a -r ecbfe2645694 doc-src/TutorialI/Protocol/Public.thy
--- a/doc-src/TutorialI/Protocol/Public.thy	Thu Jan 31 01:31:19 2008 +0100
+++ b/doc-src/TutorialI/Protocol/Public.thy	Thu Jan 31 09:16:01 2008 +0100
@@ -155,7 +155,7 @@
 ML {*
 fun possibility_tac st = st |>
     REPEAT (*omit used_Says so that Nonces start from different traces!*)
-    (ALLGOALS (simp_tac (simpset() delsimps [used_Says]))
+    (ALLGOALS (simp_tac (@{simpset} delsimps [used_Says]))
      THEN
      REPEAT_FIRST (eq_assume_tac ORELSE' 
                    resolve_tac [refl, conjI, @{thm Nonce_supply}]));