1.1 --- a/src/Tools/isac/Interpret/rewtools.sml	Fri Jun 21 11:19:18 2013 +0200
     1.2 +++ b/src/Tools/isac/Interpret/rewtools.sml	Fri Jun 21 17:49:24 2013 +0200
     1.3 @@ -581,7 +581,7 @@
     1.4        (case applicable_in pos pt tac of
     1.5          Appl (Rewrite' (thy', ord', erls, _, (thmID,_), f, (res,asm))) =>
     1.6            let 
     1.7 -            val thmDeriv = "WN120320: get this from a reference variable ?!?"
     1.8 +            val thmDeriv = "WN120320: AT Isa2009-2-->11 BROKEN"
     1.9              val thy = assoc_thy thy'
    1.10              val thm = (norm o #prop o rep_thm o (Global_Theory.get_thm thy)) thmID
    1.11            in
    1.12 @@ -601,7 +601,7 @@
    1.13  		       end
    1.14         | Notappl _ =>
    1.15             let
    1.16 -             val thmDeriv = "WN120320: get this from a reference variable ?!?"
    1.17 +             val thmDeriv = "WN120320: AT Isa2009-2-->11 BROKEN"
    1.18               val pp = par_pblobj pt p
    1.19               val thy' = get_obj g_domID pt pp
    1.20               val f = case p_ of