1.1 --- a/test/Tools/isac/Knowledge/algein.sml	Fri Jul 22 14:01:52 2011 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/algein.sml	Mon Jul 25 08:31:53 2011 +0200
     1.3 @@ -36,17 +36,7 @@
     1.4  val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
     1.5  === inhibit exn 110722=============================================================*)
     1.6  
     1.7 -val str =
     1.8 -"Script RechnenSymbolScript (k_::bool) (q__::bool)           \
     1.9 -\(u_::bool list) (s_::bool list) (o_::bool list) (l_::real) =\
    1.10 -\ (let t_ = Take (l_ = Oben + Senkrecht + Unten);            \
    1.11 -\      sum_ = boollist2sum o_;\
    1.12 -\      t_ = Substitute [Oben = sum_] t_;\
    1.13 -\      t_ = Substitute o_ t_;\
    1.14 -\      t_ = Substitute [k_, q__] t_;\
    1.15 -\      t_ = Repeat (Try (Rewrite_Set norm_Poly False)) t_\
    1.16 -\ in t_)"
    1.17 -;
    1.18 +
    1.19  (*=== inhibit exn 110722=============================================================
    1.20  val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
    1.21