src/HOL/Modelcheck/mucke_oracle.ML

--- a/src/HOL/Modelcheck/mucke_oracle.ML	Tue Nov 24 14:37:23 2009 +0100
+++ b/src/HOL/Modelcheck/mucke_oracle.ML	Tue Nov 24 17:28:25 2009 +0100
@@ -95,7 +95,7 @@
 
 fun if_full_simp_tac sset i state =
 let val sign = Thm.theory_of_thm state;
-        val (subgoal::_) = Library.drop(i-1,prems_of state);
+        val subgoal = nth (prems_of state) i;
         val prems = Logic.strip_imp_prems subgoal;
         val concl = Logic.strip_imp_concl subgoal;
         val prems = prems @ [concl];