tuned;

--- a/src/HOL/Algebra/abstract/Ring.thy	Thu Jul 08 19:32:46 2004 +0200
+++ b/src/HOL/Algebra/abstract/Ring.thy	Thu Jul 08 19:32:53 2004 +0200
@@ -158,15 +158,10 @@
 ML {*
   local
     val lhss = 
-        [read_cterm (sign_of (the_context ()))
-                    ("?t + ?u::'a::ring", TVar (("'z", 0), [])),
-	 read_cterm (sign_of (the_context ()))
-                    ("?t - ?u::'a::ring", TVar (("'z", 0), [])),
-	 read_cterm (sign_of (the_context ()))
-                    ("?t * ?u::'a::ring", TVar (("'z", 0), [])),
-	 read_cterm (sign_of (the_context ()))
-                    ("- ?t::'a::ring", TVar (("'z", 0), []))
-	];
+        ["t + u::'a::ring",
+	 "t - u::'a::ring",
+	 "t * u::'a::ring",
+	 "- t::'a::ring"];
     fun proc sg _ t = 
       let val rew = Tactic.prove sg [] []
             (HOLogic.mk_Trueprop
@@ -179,7 +174,7 @@
         else Some rew 
     end;
   in
-    val ring_simproc = mk_simproc "ring" lhss proc;
+    val ring_simproc = Simplifier.simproc (sign_of (the_context ())) "ring" lhss proc;
   end;
 *}