--- 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)
--- 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