diff -r a8481da77270 -r 0878aecbf119 src/HOL/Tools/Function/function.ML
--- a/src/HOL/Tools/Function/function.ML	Tue Nov 17 14:51:32 2009 +0100
+++ b/src/HOL/Tools/Function/function.ML	Tue Nov 17 14:51:57 2009 +0100
@@ -20,8 +20,6 @@
 
     val termination_proof : term option -> local_theory -> Proof.state
     val termination_proof_cmd : string option -> local_theory -> Proof.state
-    val termination : term option -> local_theory -> Proof.state
-    val termination_cmd : string option -> local_theory -> Proof.state
 
     val setup : theory -> theory
     val get_congs : Proof.context -> thm list
@@ -119,7 +117,6 @@
         end
     in
       lthy
-        |> is_external ? Local_Theory.set_group (serial ())
         |> Proof.theorem_i NONE afterqed [[(Logic.unprotect (concl_of goalstate), [])]]
         |> Proof.refine (Method.primitive_text (fn _ => goalstate)) |> Seq.hd
     end
@@ -170,18 +167,8 @@
       |> Proof.theorem_i NONE afterqed [[(goal, [])]]
     end
 
-val termination_proof = gen_termination_proof Syntax.check_term;
-val termination_proof_cmd = gen_termination_proof Syntax.read_term;
-
-fun termination term_opt lthy =
-  lthy
-  |> Local_Theory.set_group (serial ())
-  |> termination_proof term_opt;
-
-fun termination_cmd term_opt lthy =
-  lthy
-  |> Local_Theory.set_group (serial ())
-  |> termination_proof_cmd term_opt;
+val termination_proof = gen_termination_proof Syntax.check_term
+val termination_proof_cmd = gen_termination_proof Syntax.read_term
 
 
 (* Datatype hook to declare datatype congs as "function_congs" *)
@@ -217,13 +204,13 @@
 val _ =
   OuterSyntax.local_theory_to_proof "function" "define general recursive functions" K.thy_goal
   (function_parser default_config
-     >> (fn ((config, fixes), statements) => add_function_cmd fixes statements config));
+     >> (fn ((config, fixes), statements) => add_function_cmd fixes statements config))
 
 val _ =
   OuterSyntax.local_theory_to_proof "termination" "prove termination of a recursive function" K.thy_goal
-  (Scan.option P.term >> termination_cmd);
+  (Scan.option P.term >> termination_proof_cmd)
 
-end;
+end
 
 
 end