# HG changeset patch
# User krauss
# Date 1272469357 -7200
# Node ID a294e4ebe0a3ef7dc3dc9c0d547c0a980fe48252
# Parent  e80a95279ef63ff40f3babd28ca131dd3c033750
clarified signature; simpler implementation in terms of function's tactic interface

diff -r e80a95279ef6 -r a294e4ebe0a3 src/HOL/Tools/Function/fun.ML
--- a/src/HOL/Tools/Function/fun.ML	Wed Apr 28 16:13:17 2010 +0200
+++ b/src/HOL/Tools/Function/fun.ML	Wed Apr 28 17:42:37 2010 +0200
@@ -7,12 +7,12 @@
 
 signature FUNCTION_FUN =
 sig
-  val add_fun : Function_Common.function_config ->
-    (binding * typ option * mixfix) list -> (Attrib.binding * term) list ->
-    bool -> local_theory -> Proof.context
-  val add_fun_cmd : Function_Common.function_config ->
-    (binding * string option * mixfix) list -> (Attrib.binding * string) list ->
-    bool -> local_theory -> Proof.context
+  val add_fun : (binding * typ option * mixfix) list ->
+    (Attrib.binding * term) list -> Function_Common.function_config ->
+    local_theory -> Proof.context
+  val add_fun_cmd : (binding * string option * mixfix) list ->
+    (Attrib.binding * string) list -> Function_Common.function_config ->
+    local_theory -> Proof.context
 
   val setup : theory -> theory
 end
@@ -56,15 +56,6 @@
     ()
   end
 
-val by_pat_completeness_auto =
-  Proof.global_future_terminal_proof
-    (Method.Basic Pat_Completeness.pat_completeness,
-     SOME (Method.Source_i (Args.src (("HOL.auto", []), Position.none))))
-
-fun termination_by method int =
-  Function.termination NONE
-  #> Proof.global_future_terminal_proof (Method.Basic method, NONE) int
-
 fun mk_catchall fixes arity_of =
   let
     fun mk_eqn ((fname, fT), _) =
@@ -148,24 +139,32 @@
 val fun_config = FunctionConfig { sequential=true, default="%x. undefined" (*FIXME dynamic scoping*), 
   domintros=false, partials=false, tailrec=false }
 
-fun gen_fun add config fixes statements int lthy =
-  lthy
-  |> add fixes statements config
-  |> by_pat_completeness_auto int
-  |> Local_Theory.restore
-  |> termination_by (SIMPLE_METHOD o Function_Common.get_termination_prover lthy) int
+fun gen_add_fun add fixes statements config lthy =
+  let
+    fun pat_completeness_auto ctxt =
+      Pat_Completeness.pat_completeness_tac ctxt 1
+      THEN auto_tac (clasimpset_of ctxt)
+    fun prove_termination lthy =
+      Function.prove_termination NONE
+        (Function_Common.get_termination_prover lthy lthy) lthy
+  in
+    lthy
+    |> add fixes statements config pat_completeness_auto |> snd
+    |> Local_Theory.restore
+    |> prove_termination
+  end
 
-val add_fun = gen_fun Function.function
-val add_fun_cmd = gen_fun Function.function_cmd
+val add_fun = gen_add_fun Function.add_function
+val add_fun_cmd = gen_add_fun Function.add_function_cmd
 
 
 
 local structure P = OuterParse and K = OuterKeyword in
 
 val _ =
-  OuterSyntax.local_theory' "fun" "define general recursive functions (short version)" K.thy_decl
+  OuterSyntax.local_theory "fun" "define general recursive functions (short version)" K.thy_decl
   (function_parser fun_config
-     >> (fn ((config, fixes), statements) => add_fun_cmd config fixes statements));
+     >> (fn ((config, fixes), statements) => add_fun_cmd fixes statements config));
 
 end