1.1 --- a/src/Tools/isac/Knowledge/LinEq.thy	Mon Dec 31 14:15:19 2018 +0100
     1.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy	Mon Dec 31 14:49:16 2018 +0100
     1.3 @@ -34,9 +34,9 @@
     1.4  val LinEq_prls = (*3.10.02:just the following order due to subterm evaluation*)
     1.5    Rule.append_rls "LinEq_prls" Rule.e_rls 
     1.6  	     [Rule.Calc ("HOL.eq",eval_equal "#equal_"),
     1.7 -	      Rule.Calc ("Tools.matches",eval_matches ""),
     1.8 -	      Rule.Calc ("Tools.lhs"    ,eval_lhs ""),
     1.9 -	      Rule.Calc ("Tools.rhs"    ,eval_rhs ""),
    1.10 +	      Rule.Calc ("Tools.matches", Tools.eval_matches ""),
    1.11 +	      Rule.Calc ("Tools.lhs"    , Tools.eval_lhs ""),
    1.12 +	      Rule.Calc ("Tools.rhs"    , Tools.eval_rhs ""),
    1.13  	      Rule.Calc ("Poly.has'_degree'_in",eval_has_degree_in ""),
    1.14   	      Rule.Calc ("Poly.is'_polyrat'_in",eval_is_polyrat_in ""),
    1.15  	      Rule.Calc ("Atools.occurs'_in",eval_occurs_in ""),