src/HOL/Tools/Function/function_core.ML

       |> (fn it => Drule.compose_single (it, 2, acc_induct_rule)) (* "EX! y. (?x,y):G" *)
       |> (fn it => fold (Thm.forall_intr o cterm_of thy o Var) (Term.add_vars (prop_of it) []) it)
 
     val goalstate =  Conjunction.intr graph_is_function complete
       |> Thm.close_derivation
-      |> Goal.protect
+      |> Goal.protect 0
       |> fold_rev (Thm.implies_intr o cprop_of) compat
       |> Thm.implies_intr (cprop_of complete)
   in
     (goalstate, values)
   end