src/Pure/Isar/element.ML

 
 val refine_witness =
   Proof.refine (Method.Basic (K (RAW_METHOD
     (K (ALLGOALS
       (CONJUNCTS (ALLGOALS
-        (CONJUNCTS (TRYALL (Tactic.rtac Drule.protectI)))))))), Position.none));
+        (CONJUNCTS (TRYALL (Tactic.rtac Drule.protectI))))))))));
 
 fun gen_witness_proof proof after_qed wit_propss eq_props =
   let
     val propss = (map o map) (fn prop => (mark_witness prop, [])) wit_propss
       @ [map (rpair []) eq_props];