changeset 26342 | 0f65fa163304 |
parent 26336 | a0e2b706ce73 |
child 26343 | 0dd2eab7b296 |
--- a/src/HOL/Modelcheck/mucke_oracle.ML Wed Mar 19 22:47:39 2008 +0100 +++ b/src/HOL/Modelcheck/mucke_oracle.ML Wed Mar 19 22:50:42 2008 +0100 @@ -111,7 +111,7 @@ ( OldGoals.push_proof(); OldGoals.goalw_cterm [] (cterm_of sign trm); -by (simp_tac (simpset()) 1); +by (SIMPSET' simp_tac 1); let val if_tmp_result = result() in