1.1 --- a/src/Tools/isac/Interpret/generate.sml	Fri May 25 09:58:20 2012 +0200
     1.2 +++ b/src/Tools/isac/Interpret/generate.sml	Fri May 25 16:30:15 2012 +0200
     1.3 @@ -470,17 +470,18 @@
     1.4    | generate1 thy m' _ _ _ = 
     1.5        error ("generate1: not impl.for "^(tac_2str m'));
     1.6  
     1.7 -fun generate_inconsistent_rew (subs_opt, thm') (f', asm) (is, ctxt) (pos as (p,_)) pt =
     1.8 +fun generate_inconsistent_rew (subs_opt, thm') f' (is, ctxt) (pos as (p,_)) pt =
     1.9    let
    1.10 -    val f = get_curr_formula (pt, lev_back' pos)
    1.11 +    val f = get_curr_formula (pt, pos);
    1.12 +    val pos' as (p', _) = (lev_on p, Res);
    1.13      val (pt,c) = 
    1.14        case subs_opt of
    1.15 -        NONE => cappend_atomic pt p (is, insert_assumptions asm ctxt) f
    1.16 -          (Rewrite thm') (f', asm) Inconsistent
    1.17 -      | SOME subs => cappend_atomic pt p (is, insert_assumptions asm ctxt) f
    1.18 -          (Rewrite_Inst (subs, thm')) (f', asm) Inconsistent
    1.19 -    val pt = update_branch pt p TransitiveB
    1.20 -  in (pt, (p,Res)) end
    1.21 +        NONE => cappend_atomic pt p' (is, insert_assumptions [] ctxt) f
    1.22 +          (Rewrite thm') (f', []) Inconsistent
    1.23 +      | SOME subs => cappend_atomic pt p' (is, insert_assumptions [] ctxt) f
    1.24 +          (Rewrite_Inst (subs, thm')) (f', []) Inconsistent
    1.25 +    val pt = update_branch pt p' TransitiveB;
    1.26 +  in (pt, pos') end
    1.27  
    1.28  fun generate_hard thy m' (p,p_) pt =
    1.29    let