changeset 27208 | 5fe899199f85 |
parent 26359 | 6d437bde2f1d |
child 35174 | e15040ae75d7 |
--- a/src/HOLCF/IOA/meta_theory/ShortExecutions.thy Sat Jun 14 17:49:24 2008 +0200 +++ b/src/HOLCF/IOA/meta_theory/ShortExecutions.thy Sat Jun 14 23:19:51 2008 +0200 @@ -226,7 +226,7 @@ apply auto apply (rule_tac x = "filter_act$ (Cut (%a. fst a:ext A) (snd ex))" in exI) apply (simp add: executions_def) -apply (tactic {* pair_tac "ex" 1 *}) +apply (tactic {* pair_tac @{context} "ex" 1 *}) apply auto apply (rule_tac x = " (x,Cut (%a. fst a:ext A) y) " in exI) apply (simp (no_asm_simp))