| 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