--- a/src/HOLCF/IOA/NTP/Impl.thy Sat Mar 29 19:14:03 2008 +0100
+++ b/src/HOLCF/IOA/NTP/Impl.thy Sat Mar 29 19:14:05 2008 +0100
@@ -208,7 +208,7 @@
txt {* 10 cases. First 4 are simple, since state doesn't change *}
-ML {* val tac2 = asm_full_simp_tac (ss addsimps [@{thm inv2_def}]) *}
+ML_command {* val tac2 = asm_full_simp_tac (ss addsimps [@{thm inv2_def}]) *}
txt {* 10 - 7 *}
apply (tactic "EVERY1 [tac2,tac2,tac2,tac2]")
@@ -263,7 +263,7 @@
apply (simp (no_asm_simp) add: impl_ioas split del: split_if)
apply (induct_tac "a")
-ML {* val tac3 = asm_full_simp_tac (ss addsimps [@{thm inv3_def}]) *}
+ML_command {* val tac3 = asm_full_simp_tac (ss addsimps [@{thm inv3_def}]) *}
txt {* 10 - 8 *}
@@ -328,7 +328,7 @@
apply (simp (no_asm_simp) add: impl_ioas split del: split_if)
apply (induct_tac "a")
-ML {* val tac4 = asm_full_simp_tac (ss addsimps [@{thm inv4_def}]) *}
+ML_command {* val tac4 = asm_full_simp_tac (ss addsimps [@{thm inv4_def}]) *}
txt {* 10 - 2 *}