src/Pure/Isar/obtain.ML

   let
     val {thy, prop, maxidx, ...} = Thm.rep_thm thm;
     val cparms = map (Thm.cterm_of thy) parms;
 
     val thm' = thm
-      |> Drule.implies_intr_goals cprops
+      |> Drule.implies_intr_protected cprops
       |> Drule.forall_intr_list cparms
       |> Drule.forall_elim_vars (maxidx + 1);
-    val elim_tacs = replicate (length cprops) (Tactic.etac Drule.goalI);
+    val elim_tacs = replicate (length cprops) (Tactic.etac Drule.protectI);
 
     val concl = Logic.strip_assums_concl prop;
     val bads = parms inter (Term.term_frees concl);
   in
     if not (null bads) then

         Proof.fix_i (map (fn (x, T) => ([x], SOME T)) parms)
         #> Proof.assm_i (K (export_obtained state ts rule)) [(("", []), asms)]
         #> Proof.add_binds_i AutoBind.no_facts
       end;
 
-    val before_qed = SOME (Method.primitive_text (fn th =>
-      let val th' = Goal.conclude th
-      in th' COMP Drule.incr_indexes_wrt [] [] [] [th'] Drule.goalI end));
+    val before_qed = SOME (Method.primitive_text (Goal.conclude #> Goal.protect));
     fun after_qed _ [[res]] =
       (check_result res; Proof.end_block #> Seq.map (`Proof.the_fact #-> guess_context));
   in
     state
     |> Proof.enter_forward