1.1 --- a/src/Tools/isac/Interpret/generate.sml	Thu May 24 19:07:15 2012 +0200
     1.2 +++ b/src/Tools/isac/Interpret/generate.sml	Fri May 25 09:58:20 2012 +0200
     1.3 @@ -472,7 +472,7 @@
     1.4  
     1.5  fun generate_inconsistent_rew (subs_opt, thm') (f', asm) (is, ctxt) (pos as (p,_)) pt =
     1.6    let
     1.7 -    val f = get_curr_formula (pt, pos) (*already done in find_fillpatterns, too*)
     1.8 +    val f = get_curr_formula (pt, lev_back' pos)
     1.9      val (pt,c) = 
    1.10        case subs_opt of
    1.11          NONE => cappend_atomic pt p (is, insert_assumptions asm ctxt) f