src/HOL/Modelcheck/mucke_oracle.ML

 val trm = hd(itrm)
 in
 (
 OldGoals.push_proof();
 OldGoals.goalw_cterm [] (cterm_of sign trm);
-by (SIMPSET' simp_tac 1);
+by (simp_tac (simpset_of sign) 1);
         let
         val if_tmp_result = result()
         in
         (
         OldGoals.pop_proof();