src/Pure/Isar/specification.ML

             |> ProofContext.add_assms_i Assumption.assume_export
               [((name, [ContextRules.intro_query NONE]), [(asm, [])])]
             |>> (fn [(_, [th])] => th)
           end;
 
-        val atts = map Attrib.internal
+        val atts = map (Attrib.internal o K)
           [RuleCases.consumes (~ (length obtains)), RuleCases.case_names case_names];
         val prems = subtract_prems loc_ctxt elems_ctxt;
         val stmt = [(("", atts), [(thesis, [])])];
 
         val (facts, goal_ctxt) = elems_ctxt