src/HOL/Library/simps_case_conv.ML

--- a/src/HOL/Library/simps_case_conv.ML	Tue Dec 08 11:28:57 2015 +0100
+++ b/src/HOL/Library/simps_case_conv.ML	Wed Dec 09 16:22:29 2015 +0100
@@ -212,7 +212,7 @@
 fun case_of_simps_cmd (bind, thms_ref) lthy =
   let
     val bind' = apsnd (map (Attrib.check_src lthy)) bind
-    val thm = (Attrib.eval_thms lthy) thms_ref |> to_case lthy
+    val thm = Attrib.eval_thms lthy thms_ref |> to_case lthy
   in
     Local_Theory.note (bind', [thm]) lthy |> snd
   end