1.1 --- a/src/Tools/isac/Interpret/generate.sml	Thu May 24 17:13:58 2012 +0200
     1.2 +++ b/src/Tools/isac/Interpret/generate.sml	Thu May 24 18:40:07 2012 +0200
     1.3 @@ -470,12 +470,17 @@
     1.4    | generate1 thy m' _ _ _ = 
     1.5        error ("generate1: not impl.for "^(tac_2str m'));
     1.6  
     1.7 -fun generate_inconsistent _ (Rewrite' (_,_,_,_, thm', f, (f', asm))) (is, ctxt) (p,_) pt =
     1.8 -      let
     1.9 -        val (pt,c) = cappend_atomic pt p (is, insert_assumptions asm ctxt) f
    1.10 +fun generate_inconsistent_rew (subs_opt, thm') (f', asm) (is, ctxt) (pos as (p,_)) pt =
    1.11 +  let
    1.12 +    val f = get_curr_formula (pt, pos) (*already done in find_fillpatterns, too*)
    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 -        val pt = update_branch pt p TransitiveB
    1.18 -      in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')), pt)end
    1.19 +      | SOME subs => cappend_atomic pt p (is, insert_assumptions asm ctxt) f
    1.20 +          (Rewrite_Inst (subs, thm')) (f', asm) Inconsistent
    1.21 +    val pt = update_branch pt p TransitiveB
    1.22 +  in (pt, (p,Res)) end
    1.23  
    1.24  fun generate_hard thy m' (p,p_) pt =
    1.25    let