--- a/src/HOL/UNITY/UNITY_tactics.ML Thu Mar 19 17:25:57 2015 +0100
+++ b/src/HOL/UNITY/UNITY_tactics.ML Thu Mar 19 22:30:57 2015 +0100
@@ -44,9 +44,9 @@
(*now there are two subgoals: co & transient*)
simp_tac (ctxt addsimps [@{thm mk_total_program_def}]) 2,
res_inst_tac ctxt
- [(("act", 0), sact)] @{thm totalize_transientI} 2
+ [((("act", 0), Position.none), sact)] @{thm totalize_transientI} 2
ORELSE res_inst_tac ctxt
- [(("act", 0), sact)] @{thm transientI} 2,
+ [((("act", 0), Position.none), sact)] @{thm transientI} 2,
(*simplify the command's domain*)
simp_tac (ctxt addsimps @{thms Domain_unfold}) 3,
constrains_tac ctxt 1,