1.1 --- a/test/Tools/isac/Knowledge/rational-old.sml	Wed Sep 08 16:45:27 2010 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/rational-old.sml	Wed Sep 08 16:47:22 2010 +0200
     1.3 @@ -242,7 +242,7 @@
     1.4  val (t,asm) = the (rewrite_set_ thy eval_rls false rls t);
     1.5  
     1.6  
     1.7 -val thy' = "Rational.thy";
     1.8 +val thy' = "Rational";
     1.9  val rls' = "cancel";
    1.10  val t' = "(1 + 1 * a ^^^ 1)///(-2 + 2 * a ^^^ 2)";
    1.11  val (t',asm') = the (rewrite_set thy' "eval_rls" false rls' t');
    1.12 @@ -250,12 +250,12 @@
    1.13  else raise error "tests/rationals.sml(1): new behaviour";*)
    1.14  
    1.15  
    1.16 -val thy' = "Rational.thy";
    1.17 +val thy' = "Rational";
    1.18  val rls' = "cancel";
    1.19  val t' = "(10 * a^^^2 * b * c + 14 * a * b + 3 * a * c + 20 * a * b^^^2 * c) /// (5 * a * b * c  +  7 * a^^^2 * b * c) ";
    1.20  val (t',asm') = the (rewrite_set thy' "eval_rls" false rls' t');
    1.21  
    1.22 -val thy' = "Rational.thy";
    1.23 +val thy' = "Rational";
    1.24  val rls' = "cancel";
    1.25  val t' = "(a^^^2 * b  + 2 * a * b +  b ) /// ( a^^^2   - 1 )";
    1.26  val (t',asm') = the (rewrite_set thy' "eval_rls" false rls' t');
    1.27 @@ -274,7 +274,7 @@
    1.28     Schalk 
    1.29     Reniets Verlag *)
    1.30  
    1.31 -val thy' = "Rational.thy";
    1.32 +val thy' = "Rational";
    1.33  val rls' = "cancel";
    1.34  val mp = "make_polynomial";
    1.35