val t = str2term "(hd o (filterVar (f_f::real))) (eqs::bool list)";

 val t = str2term "(hd o (filterVar (f_f::real))) (eqs::bool list)";

 val s = subst_atomic env t;

 val s = subst_atomic env t;

 term2str s;

 term2str s;

 val t = str2term 

 val t = str2term 

 "(hd o filterVar A) [A = a * b, a / 2 = r * sin alpha, b / 2 = r * cos alpha]";

 "(hd o filterVar A) [A = a * b, a / 2 = r * sin alpha, b / 2 = r * cos alpha]";

 val SOME (t',_) = rewrite_set_ thy false list_rls t;

 val SOME (t',_) = rewrite_set_ thy false list_rls t;

 trace_rewrite:=false;

 trace_rewrite:=false;

 val s' = term2str t';

 val s' = term2str t';

 (*=== inhibit exn 110726=============================================================

 (*=== inhibit exn 110726=============================================================

 if s' = "A = a * b" then() else error "new behaviour with list_rls 3.1.";

 if s' = "A = a * b" then() else error "new behaviour with list_rls 3.1.";