src/HOL/ex/svc_funcs.ML
changeset 44064 5bce8ff0d9ae
parent 43850 7f2cbc713344
child 51940 958d439b3013
--- a/src/HOL/ex/svc_funcs.ML	Mon Aug 08 08:55:49 2011 -0700
+++ b/src/HOL/ex/svc_funcs.ML	Mon Aug 08 09:52:09 2011 -0700
@@ -173,7 +173,7 @@
       | tm (Const(@{const_name Groups.times}, T) $ x $ y) =
           if is_numeric_op T then Interp("*", [tm x, tm y])
           else fail t
-      | tm (Const(@{const_name Rings.inverse}, T) $ x) =
+      | tm (Const(@{const_name Fields.inverse}, T) $ x) =
           if domain_type T = HOLogic.realT then
               Rat(1, litExp x)
           else fail t