1.1 --- a/src/Tools/isac/Interpret/generate.sml	Tue May 22 07:00:53 2012 +0200
     1.2 +++ b/src/Tools/isac/Interpret/generate.sml	Tue May 22 13:40:06 2012 +0200
     1.3 @@ -389,7 +389,7 @@
     1.4          val (pt,c) = cappend_atomic pt p (is, insert_assumptions asm ctxt) f
     1.5            (Rewrite thm') (f',asm) Complete
     1.6          val pt = update_branch pt p TransitiveB
     1.7 -      in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')), pt)end
     1.8 +      in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')), pt) end
     1.9  
    1.10    | generate1 thy (Rewrite_Asm' all) l p pt = generate1 thy (Rewrite' all) l p pt
    1.11  
    1.12 @@ -470,6 +470,13 @@
    1.13    | generate1 thy m' _ _ _ = 
    1.14        error ("generate1: not impl.for "^(tac_2str m'));
    1.15  
    1.16 +fun generate_inconsistent _ (Rewrite' (_,_,_,_, thm', f, (f', asm))) (is, ctxt) (p,_) pt =
    1.17 +      let
    1.18 +        val (pt,c) = cappend_atomic pt p (is, insert_assumptions asm ctxt) f
    1.19 +          (Rewrite thm') (f', asm) Inconsistent
    1.20 +        val pt = update_branch pt p TransitiveB
    1.21 +      in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')), pt)end
    1.22 +
    1.23  fun generate_hard thy m' (p,p_) pt =
    1.24    let  
    1.25      val p =