# HG changeset patch
# User wenzelm
# Date 1089307973 -7200
# Node ID fcbc73812e6c891a05d99af6d7579ad9649ddb07
# Parent  acf67fa3099893d2ddc850cc76a9ab4c3a5f5628
tuned;

diff -r acf67fa30998 -r fcbc73812e6c src/HOL/Algebra/abstract/Ring.thy
--- 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;
 *}