# HG changeset patch
# User wenzelm
# Date 1449674549 -3600
# Node ID b84688dd7f6b28fea7b9ab7293fe926dfae4a613
# Parent  71446a608dfdc991b7477acbba628afd9e1c1f92
tuned;

diff -r 71446a608dfd -r b84688dd7f6b src/HOL/Eisbach/Tests.thy
--- a/src/HOL/Eisbach/Tests.thy	Tue Dec 08 11:28:57 2015 +0100
+++ b/src/HOL/Eisbach/Tests.thy	Wed Dec 09 16:22:29 2015 +0100
@@ -480,7 +480,7 @@
 
 subsection \<open>Shallow parser tests\<close>
 
-method all_args for A B methods m1 m2 uses f1 f2 declares my_thms_named = (fail)
+method all_args for A B methods m1 m2 uses f1 f2 declares my_thms_named = fail
 
 lemma True
   by (all_args True False \<open>-\<close> \<open>fail\<close> f1: TrueI f2: TrueI my_thms_named: TrueI | rule TrueI)
diff -r 71446a608dfd -r b84688dd7f6b 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