# HG changeset patch
# User wenzelm
# Date 1221679638 -7200
# Node ID 7e14443f2dd6ec44db8740276ebc0815852b84d9
# Parent  e1dae766c108d79622bda85d9873567c59105efb
use ML_prf within proofs;

diff -r e1dae766c108 -r 7e14443f2dd6 src/HOLCF/IOA/NTP/Impl.thy
--- a/src/HOLCF/IOA/NTP/Impl.thy	Wed Sep 17 21:27:17 2008 +0200
+++ b/src/HOLCF/IOA/NTP/Impl.thy	Wed Sep 17 21:27:18 2008 +0200
@@ -199,7 +199,7 @@
 
   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]")
@@ -255,7 +255,7 @@
   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 *}
 
@@ -320,7 +320,7 @@
   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 *}