changeset 51717 | 9e7d1c139569 |
parent 44766 | d4d33a4d7548 |
child 56544 | b60d5d119489 |
--- a/src/HOL/Old_Number_Theory/Chinese.thy Tue Apr 16 17:54:14 2013 +0200 +++ b/src/HOL/Old_Number_Theory/Chinese.thy Thu Apr 18 17:07:01 2013 +0200 @@ -243,7 +243,7 @@ prefer 6 apply (simp add: mult_ac) apply (unfold xilin_sol_def) - apply (tactic {* asm_simp_tac @{simpset} 6 *}) + apply (tactic {* asm_simp_tac @{context} 6 *}) apply (rule_tac [6] ex1_implies_ex [THEN someI_ex]) apply (rule_tac [6] unique_xi_sol) apply (rule_tac [3] funprod_zdvd)