# HG changeset patch
# User haftmann
# Date 1178605299 -7200
# Node ID 3dd306cb98d2b2dac078b8478fd7d03cfc04d378
# Parent  8ec47039614ef8786f342072cfa2926c1e367441
ML adaptions

diff -r 8ec47039614e -r 3dd306cb98d2 doc-src/TutorialI/Protocol/Message_lemmas.ML
--- a/doc-src/TutorialI/Protocol/Message_lemmas.ML	Tue May 08 05:30:10 2007 +0200
+++ b/doc-src/TutorialI/Protocol/Message_lemmas.ML	Tue May 08 08:21:39 2007 +0200
@@ -849,7 +849,7 @@
   concerns  Crypt K X \\<notin> Key`shrK`bad  and cannot be proved by rewriting
   alone.*)
 fun prove_simple_subgoals_tac i = 
-    force_tac (claset(), simpset() addsimps [image_eq_UN]) i THEN
+    force_tac (claset(), simpset() addsimps [@{thm image_eq_UN}]) i THEN
     ALLGOALS Asm_simp_tac;
 
 fun Fake_parts_insert_tac i = 
diff -r 8ec47039614e -r 3dd306cb98d2 doc-src/TutorialI/Protocol/Public_lemmas.ML
--- a/doc-src/TutorialI/Protocol/Public_lemmas.ML	Tue May 08 05:30:10 2007 +0200
+++ b/doc-src/TutorialI/Protocol/Public_lemmas.ML	Tue May 08 08:21:39 2007 +0200
@@ -13,7 +13,7 @@
 
 (*** Basic properties of pubK & priK ***)
 
-AddIffs [inj_pubK RS inj_eq];
+AddIffs [inj_pubK RS @{thm inj_eq}];
 
 Goal "(priK A = priK B) = (A=B)";
 by Safe_tac;