diff -r cd7854f2636d -r 02a9b2540eb7 src/Tools/isac/Knowledge/Poly.thy
--- a/src/Tools/isac/Knowledge/Poly.thy	Tue Sep 28 13:30:29 2010 +0200
+++ b/src/Tools/isac/Knowledge/Poly.thy	Fri Oct 01 10:23:38 2010 +0200
@@ -1346,15 +1346,18 @@
 val order_mult_ =
     Rrls {id = "order_mult_", 
 	  prepat = 
+          (* ?p matched with the current term gives an environment,
+             which evaluates (the instantiated) "p is_multUnordered" to true*)
 	  [([(term_of o the o (parse thy)) "p is_multUnordered"], 
-	    parse_patt thy "?p" )],
+	    parse_patt thy "?p :: real" )],
 	  rew_ord = ("dummy_ord", dummy_ord),
 	  erls = append_rls "e_rls-is_multUnordered" e_rls(*MG: poly_erls*)
 			    [Calc ("Poly.is'_multUnordered", 
                                     eval_is_multUnordered "")],
-	  calc = [("PLUS"  , ("Groups.plus_class.plus"      , eval_binop "#add_")),
-		  ("TIMES" , ("Groups.times_class.times"      , eval_binop "#mult_")),
-		  ("DIVIDE", ("Rings.inverse_class.divide", eval_cancel "#divide_e")),
+	  calc = [("PLUS"  , ("Groups.plus_class.plus", eval_binop "#add_")),
+		  ("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")),
+		  ("DIVIDE", ("Rings.inverse_class.divide", 
+		              eval_cancel "#divide_e")),
 		  ("POWER" , ("Atools.pow", eval_binop "#power_"))],
 	  scr=Rfuns {init_state  = init_state,
 		     normal_form = normal_form,