changeset 32149 | ef59550a55d3 |
parent 30607 | c3d1590debd8 |
child 32174 | 9036cc8ae775 |
--- a/src/HOL/Modelcheck/mucke_oracle.ML Thu Jul 23 18:44:08 2009 +0200 +++ b/src/HOL/Modelcheck/mucke_oracle.ML Thu Jul 23 18:44:09 2009 +0200 @@ -109,7 +109,7 @@ ( OldGoals.push_proof(); OldGoals.goalw_cterm [] (cterm_of sign trm); -by (simp_tac (simpset_of sign) 1); +by (simp_tac (global_simpset_of sign) 1); let val if_tmp_result = result() in