test/Tools/isac/Knowledge/rational.sml
branchisac-update-Isa09-2
changeset 37969 81922154e742
parent 37967 bd4f7a35e892
child 37979 4f11d7840684
     1.1 --- a/test/Tools/isac/Knowledge/rational.sml	Wed Sep 01 09:56:09 2010 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/rational.sml	Wed Sep 01 15:17:43 2010 +0200
     1.3 @@ -983,7 +983,7 @@
     1.4  "True";
     1.5  val t = str2term "(6*x)^^^2";
     1.6  val SOME (t',_) = rewrite_ thy dummy_ord powers_erls false 
     1.7 -			   (num_str @{realpow_def_atom) t;
     1.8 +			   (num_str @{thm realpow_def_atom) t;
     1.9  term2str t';
    1.10  trace_rewrite:=false;
    1.11