src/HOL/Tools/Function/fun.ML

--- a/src/HOL/Tools/Function/fun.ML	Fri Oct 23 15:33:19 2009 +0200
+++ b/src/HOL/Tools/Function/fun.ML	Fri Oct 23 16:22:10 2009 +0200
@@ -7,10 +7,10 @@
 
 signature FUNCTION_FUN =
 sig
-    val add_fun : FundefCommon.fundef_config ->
+    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 : FundefCommon.fundef_config ->
+    val add_fun_cmd : Function_Common.function_config ->
       (binding * string option * mixfix) list -> (Attrib.binding * string) list ->
       bool -> local_theory -> Proof.context
 
@@ -20,8 +20,8 @@
 structure Function_Fun : FUNCTION_FUN =
 struct
 
-open FundefLib
-open FundefCommon
+open Function_Lib
+open Function_Common
 
 
 fun check_pats ctxt geq =
@@ -62,7 +62,7 @@
        SOME (Method.Source_i (Args.src (("HOL.auto", []), Position.none))))
 
 fun termination_by method int =
-    Fundef.termination_proof NONE
+    Function.termination_proof NONE
     #> Proof.global_future_terminal_proof (Method.Basic method, NONE) int
 
 fun mk_catchall fixes arity_of =
@@ -104,7 +104,7 @@
     end
 
 
-fun sequential_preproc (config as FundefConfig {sequential, ...}) ctxt fixes spec =
+fun sequential_preproc (config as FunctionConfig {sequential, ...}) ctxt fixes spec =
       if sequential then
         let
           val (bnds, eqss) = split_list spec
@@ -118,7 +118,7 @@
           val compleqs = add_catchall ctxt fixes feqs   (* Completion *)
 
           val spliteqs = warn_if_redundant ctxt feqs
-                           (FundefSplit.split_all_equations ctxt compleqs)
+                           (Function_Split.split_all_equations ctxt compleqs)
 
           fun restore_spec thms =
               bnds ~~ Library.take (length bnds, Library.unflat spliteqs thms)
@@ -141,13 +141,13 @@
           (flat spliteqs, restore_spec, sort, case_names)
         end
       else
-        FundefCommon.empty_preproc check_defs config ctxt fixes spec
+        Function_Common.empty_preproc check_defs config ctxt fixes spec
 
 val setup =
-  Context.theory_map (FundefCommon.set_preproc sequential_preproc)
+  Context.theory_map (Function_Common.set_preproc sequential_preproc)
 
 
-val fun_config = FundefConfig { sequential=true, default="%x. undefined" (*FIXME dynamic scoping*), 
+val fun_config = FunctionConfig { sequential=true, default="%x. undefined" (*FIXME dynamic scoping*), 
                                 domintros=false, tailrec=false }
 
 fun gen_fun add config fixes statements int lthy =
@@ -158,11 +158,11 @@
       |> by_pat_completeness_auto int
       |> LocalTheory.restore
       |> LocalTheory.set_group group
-      |> termination_by (FundefCommon.get_termination_prover lthy) int
+      |> termination_by (Function_Common.get_termination_prover lthy) int
   end;
 
-val add_fun = gen_fun Fundef.add_fundef
-val add_fun_cmd = gen_fun Fundef.add_fundef_cmd
+val add_fun = gen_fun Function.add_function
+val add_fun_cmd = gen_fun Function.add_function_cmd
 
 
 
@@ -170,7 +170,7 @@
 
 val _ =
   OuterSyntax.local_theory' "fun" "define general recursive functions (short version)" K.thy_decl
-  (fundef_parser fun_config
+  (function_parser fun_config
      >> (fn ((config, fixes), statements) => add_fun_cmd config fixes statements));
 
 end