equal
deleted
inserted
replaced
44 let |
44 let |
45 val goals = |
45 val goals = |
46 Drule.strip_imp_prems (Thm.cprop_of st) |
46 Drule.strip_imp_prems (Thm.cprop_of st) |
47 |> map (Thm.adjust_maxidx_cterm ~1); |
47 |> map (Thm.adjust_maxidx_cterm ~1); |
48 in |
48 in |
49 if Multithreading.relevant goals andalso forall (fn g => Thm.maxidx_of_cterm g = ~1) goals then |
49 if Future.relevant goals andalso forall (fn g => Thm.maxidx_of_cterm g = ~1) goals then |
50 let |
50 let |
51 fun try_goal g = |
51 fun try_goal g = |
52 (case SINGLE tac (Goal.init g) of |
52 (case SINGLE tac (Goal.init g) of |
53 NONE => raise FAILED () |
53 NONE => raise FAILED () |
54 | SOME st' => st'); |
54 | SOME st' => st'); |