450 | strip Hs B = rev Hs |
450 | strip Hs B = rev Hs |
451 in strip [] B end; |
451 in strip [] B end; |
452 |
452 |
453 (*Strips assumptions in goal, yielding conclusion. *) |
453 (*Strips assumptions in goal, yielding conclusion. *) |
454 fun strip_assums_concl (Const("Pure.imp", _) $ H $ B) = strip_assums_concl B |
454 fun strip_assums_concl (Const("Pure.imp", _) $ H $ B) = strip_assums_concl B |
455 | strip_assums_concl (Const("Pure.all",_)$Abs(a,T,t)) = strip_assums_concl t |
455 | strip_assums_concl (Const("Pure.all", _) $ Abs (a, T, t)) = strip_assums_concl t |
456 | strip_assums_concl B = B; |
456 | strip_assums_concl B = B; |
457 |
457 |
458 (*Make a list of all the parameters in a subgoal, even if nested*) |
458 (*Make a list of all the parameters in a subgoal, even if nested*) |
459 fun strip_params (Const("Pure.imp", _) $ H $ B) = strip_params B |
459 fun strip_params (Const("Pure.imp", _) $ H $ B) = strip_params B |
460 | strip_params (Const("Pure.all",_)$Abs(a,T,t)) = (a,T) :: strip_params t |
460 | strip_params (Const("Pure.all", _) $ Abs (a, T, t)) = (a, T) :: strip_params t |
461 | strip_params B = []; |
461 | strip_params B = []; |
462 |
462 |
463 (*test for nested meta connectives in prems*) |
463 (*test for nested meta connectives in prems*) |
464 val has_meta_prems = |
464 val has_meta_prems = |
465 let |
465 let |