equal
deleted
inserted
replaced
608 |
608 |
609 fun gen_shuffle_tac ctxt search thms i st = |
609 fun gen_shuffle_tac ctxt search thms i st = |
610 let |
610 let |
611 val thy = Proof_Context.theory_of ctxt |
611 val thy = Proof_Context.theory_of ctxt |
612 val _ = message ("Shuffling " ^ (string_of_thm st)) |
612 val _ = message ("Shuffling " ^ (string_of_thm st)) |
613 val t = List.nth(prems_of st,i-1) |
613 val t = nth (prems_of st) (i - 1) |
614 val set = set_prop thy t |
614 val set = set_prop thy t |
615 fun process_tac thms st = |
615 fun process_tac thms st = |
616 case set thms of |
616 case set thms of |
617 SOME (_,th) => Seq.of_list (compose (th,i,st)) |
617 SOME (_,th) => Seq.of_list (compose (th,i,st)) |
618 | NONE => Seq.empty |
618 | NONE => Seq.empty |