equal
deleted
inserted
replaced
326 | non_atomic (Const ("Pure.all", _) $ _) = true |
326 | non_atomic (Const ("Pure.all", _) $ _) = true |
327 | non_atomic _ = false; |
327 | non_atomic _ = false; |
328 |
328 |
329 fun assume_rule_tac ctxt = norm_hhf_tac ctxt THEN' CSUBGOAL (fn (goal, i) => |
329 fun assume_rule_tac ctxt = norm_hhf_tac ctxt THEN' CSUBGOAL (fn (goal, i) => |
330 let |
330 let |
331 val ((_, goal'), ctxt') = Variable.focus_cterm goal ctxt; |
331 val ((_, goal'), ctxt') = Variable.focus_cterm NONE goal ctxt; |
332 val goal'' = Drule.cterm_rule (singleton (Variable.export ctxt' ctxt)) goal'; |
332 val goal'' = Drule.cterm_rule (singleton (Variable.export ctxt' ctxt)) goal'; |
333 val Rs = filter (non_atomic o Thm.term_of) (Drule.strip_imp_prems goal''); |
333 val Rs = filter (non_atomic o Thm.term_of) (Drule.strip_imp_prems goal''); |
334 val tacs = Rs |> map (fn R => |
334 val tacs = Rs |> map (fn R => |
335 eresolve_tac ctxt [Raw_Simplifier.norm_hhf ctxt (Thm.trivial R)] THEN_ALL_NEW assume_tac ctxt); |
335 eresolve_tac ctxt [Raw_Simplifier.norm_hhf ctxt (Thm.trivial R)] THEN_ALL_NEW assume_tac ctxt); |
336 in fold_rev (curry op APPEND') tacs (K no_tac) i end); |
336 in fold_rev (curry op APPEND') tacs (K no_tac) i end); |