src/HOLCF/IOA/NTP/Impl.thy

   apply (simp (no_asm_simp) add: impl_ioas split del: split_if)
   apply (induct_tac "a")
 
   txt {* 10 cases. First 4 are simple, since state doesn't change *}
 
-ML_command {* val tac2 = asm_full_simp_tac (ss addsimps [@{thm inv2_def}]) *}
+  ML_prf {* val tac2 = asm_full_simp_tac (ss addsimps [@{thm inv2_def}]) *}
 
   txt {* 10 - 7 *}
   apply (tactic "EVERY1 [tac2,tac2,tac2,tac2]")
   txt {* 6 *}
   apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv1_def}]

   apply (simp add: Impl.inv3_def receiver_projections sender_projections impl_ioas)
 
   apply (simp (no_asm_simp) add: impl_ioas split del: split_if)
   apply (induct_tac "a")
 
-ML_command {* val tac3 = asm_full_simp_tac (ss addsimps [@{thm inv3_def}]) *}
+  ML_prf {* val tac3 = asm_full_simp_tac (ss addsimps [@{thm inv3_def}]) *}
 
   txt {* 10 - 8 *}
 
   apply (tactic "EVERY1[tac3,tac3,tac3]")
 

   apply (simp add: Impl.inv4_def receiver_projections sender_projections impl_ioas)
 
   apply (simp (no_asm_simp) add: impl_ioas split del: split_if)
   apply (induct_tac "a")
 
-ML_command {* val tac4 =  asm_full_simp_tac (ss addsimps [@{thm inv4_def}]) *}
+  ML_prf {* val tac4 =  asm_full_simp_tac (ss addsimps [@{thm inv4_def}]) *}
 
   txt {* 10 - 2 *}
 
   apply (tactic "EVERY1[tac4,tac4,tac4,tac4,tac4,tac4,tac4,tac4,tac4]")