# HG changeset patch
# User wneuper
# Date 1162560632 -3600
# Node ID 6361fdad1d9468098dfe72dbca015b13dc423364
# Parent  0bf7c1333a3526ed930d053654e42bde54604b08
made [simplification,for_polynomials] ready for inform

diff -r 0bf7c1333a35 -r 6361fdad1d94 src/sml/IsacKnowledge/Poly.ML
--- a/src/sml/IsacKnowledge/Poly.ML	Fri Nov 03 10:51:51 2006 +0100
+++ b/src/sml/IsacKnowledge/Poly.ML	Fri Nov 03 14:30:32 2006 +0100
@@ -1479,7 +1479,7 @@
 		prls = append_rls "simplification_for_polynomials_prls" e_rls 
 				  [(*for preds in where_*)
 				   Calc ("Poly.is'_polyexp",eval_is_polyexp"")],
-		crls = e_rls, nrls = e_rls},
+		crls = e_rls, nrls = norm_Poly},
 	       "Script SimplifyScript (t_::real) =                \
 	       \  ((Rewrite_Set norm_Poly False) t_)"
 	       ));