src/Pure/Isar/element.ML

       let val (wits, eqs) = split_last ((map o map) Thm.close_derivation thmss);
       in after_qed ((map2 o map2) (curry Witness) wit_propss wits) eqs end;
   in proof after_qed' propss #> refine_witness #> Seq.hd end;
 
 fun proof_local cmd goal_ctxt int after_qed' propss =
-    Proof.map_context (K goal_ctxt)
-    #> Proof.local_goal (Proof_Display.print_results int) (K I) Proof_Context.bind_propp_i
-      cmd NONE after_qed' (map (pair Thm.empty_binding) propss);
+  Proof.map_context (K goal_ctxt) #>
+  Proof.local_goal (Proof_Display.print_results int) (K I) Proof_Context.bind_propp_i
+    cmd NONE after_qed' (map (pair Thm.empty_binding) propss);
 
 in
 
 fun witness_proof after_qed wit_propss =
   gen_witness_proof (Proof.theorem NONE) (fn wits => fn _ => after_qed wits)