equal
deleted
inserted
replaced
470 | generate1 thy m' _ _ _ = |
470 | generate1 thy m' _ _ _ = |
471 error ("generate1: not impl.for "^(tac_2str m')); |
471 error ("generate1: not impl.for "^(tac_2str m')); |
472 |
472 |
473 fun generate_inconsistent_rew (subs_opt, thm') (f', asm) (is, ctxt) (pos as (p,_)) pt = |
473 fun generate_inconsistent_rew (subs_opt, thm') (f', asm) (is, ctxt) (pos as (p,_)) pt = |
474 let |
474 let |
475 val f = get_curr_formula (pt, pos) (*already done in find_fillpatterns, too*) |
475 val f = get_curr_formula (pt, lev_back' pos) |
476 val (pt,c) = |
476 val (pt,c) = |
477 case subs_opt of |
477 case subs_opt of |
478 NONE => cappend_atomic pt p (is, insert_assumptions asm ctxt) f |
478 NONE => cappend_atomic pt p (is, insert_assumptions asm ctxt) f |
479 (Rewrite thm') (f', asm) Inconsistent |
479 (Rewrite thm') (f', asm) Inconsistent |
480 | SOME subs => cappend_atomic pt p (is, insert_assumptions asm ctxt) f |
480 | SOME subs => cappend_atomic pt p (is, insert_assumptions asm ctxt) f |