src/Pure/Isar/proof.ML

     goal_state
     |> map_context (Variable.set_body true)
     |> put_goal (SOME (make_goal ((kind, propss'), [], goal, before_qed, after_qed')))
     |> map_context (ProofContext.add_cases false (AutoBind.cases thy props))
     |> map_context (ProofContext.auto_bind_goal props)
-    |> K chaining ? (`the_facts #-> using_facts)
+    |> chaining ? (`the_facts #-> using_facts)
     |> put_facts NONE
     |> open_block
     |> put_goal NONE
     |> enter_backward
-    |> K (not (null vars)) ? refine_terms (length propss')
-    |> K (null props) ? (refine (Method.Basic Method.assumption) #> Seq.hd)
+    |> not (null vars) ? refine_terms (length propss')
+    |> null props ? (refine (Method.Basic Method.assumption) #> Seq.hd)
   end;
 
 fun generic_qed state =
   let
     val (goal_ctxt, {statement = (_, stmt), using = _, goal, before_qed = _, after_qed}) =

       refine_goals print_rule (context_of state) (flat results)
       #> Seq.maps (after_qed results);
   in
     state
     |> local_goal print_results prep_att prepp "show" before_qed after_qed' stmt
-    |> K int ? (fn goal_state =>
+    |> int ? (fn goal_state =>
       (case test_proof goal_state of
         Result (SOME _) => goal_state
       | Result NONE => error (fail_msg (context_of goal_state))
       | Exn Interrupt => raise Interrupt
       | Exn exn => raise EXCEPTION (exn, fail_msg (context_of goal_state))))