src/HOL/Tools/Function/fun.ML

       Function.prove_termination NONE
         (Function_Common.get_termination_prover lthy lthy) lthy
   in
     lthy
     |> add pat_completeness_auto |> snd
-    |> Local_Theory.restore
     |> prove_termination |> snd
   end
 
 fun add_fun a b c = gen_add_fun (Function.add_function a b c)
 fun add_fun_cmd a b c int = gen_add_fun (fn tac => Function.add_function_cmd a b c tac int)