src/HOL/Modelcheck/MuckeSyn.thy
changeset 33955 fff6f11b1f09
parent 33035 15eab423e573
child 35109 0015a0a99ae9
     1.1 --- a/src/HOL/Modelcheck/MuckeSyn.thy	Tue Nov 24 14:37:23 2009 +0100
     1.2 +++ b/src/HOL/Modelcheck/MuckeSyn.thy	Tue Nov 24 17:28:25 2009 +0100
     1.3 @@ -130,7 +130,7 @@
     1.4  
     1.5  fun move_mus i state =
     1.6  let val sign = Thm.theory_of_thm state;
     1.7 -    val (subgoal::_) = Library.drop(i-1,prems_of state);
     1.8 +    val subgoal = nth (prems_of state) i;
     1.9      val concl = Logic.strip_imp_concl subgoal; (* recursive mu's in prems? *)
    1.10      val redex = search_mu concl;
    1.11      val idx = let val t = #maxidx (rep_thm state) in 
    1.12 @@ -222,9 +222,9 @@
    1.13  (* the interface *)
    1.14  
    1.15  fun mc_mucke_tac defs i state =
    1.16 -  (case Library.drop (i - 1, Thm.prems_of state) of
    1.17 -    [] => no_tac state
    1.18 -  | subgoal :: _ =>
    1.19 +  (case try (nth (Thm.prems_of state)) i of
    1.20 +    NONE => no_tac state
    1.21 +  | SOME subgoal =>
    1.22        EVERY [
    1.23          REPEAT (etac thin_rl i),
    1.24          cut_facts_tac (mk_lam_defs defs) i,