# HG changeset patch
# User krauss
# Date 1272440902 -7200
# Node ID 46bf776a81e0dae4d44619b6d89cfdb8d7a75ded
# Parent  a33b986f2e22d7a2d71fb398a2588559411865db
ML interface uses plain command names, following conventions from typedef

diff -r a33b986f2e22 -r 46bf776a81e0 src/HOL/Tools/Function/fun.ML
--- a/src/HOL/Tools/Function/fun.ML	Wed Apr 28 09:21:48 2010 +0200
+++ b/src/HOL/Tools/Function/fun.ML	Wed Apr 28 09:48:22 2010 +0200
@@ -62,7 +62,7 @@
      SOME (Method.Source_i (Args.src (("HOL.auto", []), Position.none))))
 
 fun termination_by method int =
-  Function.termination_proof NONE
+  Function.termination NONE
   #> Proof.global_future_terminal_proof (Method.Basic method, NONE) int
 
 fun mk_catchall fixes arity_of =
@@ -155,8 +155,8 @@
   |> Local_Theory.restore
   |> termination_by (Function_Common.get_termination_prover lthy) int
 
-val add_fun = gen_fun Function.add_function
-val add_fun_cmd = gen_fun Function.add_function_cmd
+val add_fun = gen_fun Function.function
+val add_fun_cmd = gen_fun Function.function_cmd
 
 
 
diff -r a33b986f2e22 -r 46bf776a81e0 src/HOL/Tools/Function/function.ML
--- a/src/HOL/Tools/Function/function.ML	Wed Apr 28 09:21:48 2010 +0200
+++ b/src/HOL/Tools/Function/function.ML	Wed Apr 28 09:48:22 2010 +0200
@@ -9,16 +9,16 @@
 sig
   include FUNCTION_DATA
 
-  val add_function: (binding * typ option * mixfix) list ->
+  val function: (binding * typ option * mixfix) list ->
     (Attrib.binding * term) list -> Function_Common.function_config ->
     local_theory -> Proof.state
 
-  val add_function_cmd: (binding * string option * mixfix) list ->
+  val function_cmd: (binding * string option * mixfix) list ->
     (Attrib.binding * string) list -> Function_Common.function_config ->
     local_theory -> Proof.state
 
-  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
@@ -76,7 +76,7 @@
     val defname = mk_defname fixes
     val FunctionConfig {partials, ...} = config
 
-    val ((goalstate, cont), lthy) =
+    val ((goal_state, cont), lthy') =
       Function_Mutual.prepare_function_mutual config defname fixes eqs lthy
 
     fun afterqed [[proof]] lthy =
@@ -119,22 +119,22 @@
         |> Local_Theory.declaration false (add_function_data o morph_function_data info)
       end
   in 
-    ((goalstate, afterqed), lthy)
+    ((goal_state, afterqed), lthy')
   end
 
-fun gen_add_function is_external prep default_constraint fixspec eqns config lthy =
+fun gen_function is_external prep default_constraint fixspec eqns config lthy =
   let
-    val ((goalstate, afterqed), lthy') = 
+    val ((goal_state, afterqed), lthy') = 
       prepare_function is_external prep default_constraint fixspec eqns config lthy
   in
     lthy'
-    |> Proof.theorem NONE afterqed [[(Logic.unprotect (concl_of goalstate), [])]]
-    |> Proof.refine (Method.primitive_text (fn _ => goalstate)) |> Seq.hd
+    |> Proof.theorem NONE afterqed [[(Logic.unprotect (concl_of goal_state), [])]]
+    |> Proof.refine (Method.primitive_text (K goal_state)) |> Seq.hd
   end
 
-val add_function =
-  gen_add_function false Specification.check_spec (TypeInfer.anyT HOLogic.typeS)
-val add_function_cmd = gen_add_function true Specification.read_spec "_::type"
+val function =
+  gen_function false Specification.check_spec (TypeInfer.anyT HOLogic.typeS)
+val function_cmd = gen_function true Specification.read_spec "_::type"
                                                 
 fun prepare_termination_proof prep_term raw_term_opt lthy =
   let
@@ -180,7 +180,7 @@
     (goal, afterqed, termination)
   end
 
-fun gen_termination_proof prep_term raw_term_opt lthy =
+fun gen_termination prep_term raw_term_opt lthy =
   let
     val (goal, afterqed, termination) = prepare_termination_proof prep_term raw_term_opt lthy
   in
@@ -195,8 +195,8 @@
     |> Proof.theorem NONE afterqed [[(goal, [])]]
   end
 
-val termination_proof = gen_termination_proof Syntax.check_term
-val termination_proof_cmd = gen_termination_proof Syntax.read_term
+val termination = gen_termination Syntax.check_term
+val termination_cmd = gen_termination Syntax.read_term
 
 
 (* Datatype hook to declare datatype congs as "function_congs" *)
@@ -236,11 +236,11 @@
 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) => 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_proof_cmd)
+  (Scan.option P.term >> termination_cmd)
 
 end