src/HOL/Tools/function_package/fundef_datatype.ML

   let val group = serial_string () in
     lthy
       |> LocalTheory.set_group group
       |> FundefPackage.add_fundef fixes statements config flags
       |> by_pat_completeness_simp
-      |> LocalTheory.reinit
+      |> LocalTheory.restore
       |> LocalTheory.set_group group
       |> termination_by_lexicographic_order
   end;
 
 val _ =