proper signatures;

--- a/src/HOL/Tools/Function/fun.ML	Sun Oct 21 22:11:38 2012 +0200
+++ b/src/HOL/Tools/Function/fun.ML	Sun Oct 21 22:12:22 2012 +0200
@@ -157,7 +157,7 @@
       THEN auto_tac ctxt
     fun prove_termination lthy =
       Function.prove_termination NONE
-        (Function_Common.get_termination_prover lthy lthy) lthy
+        (Function_Common.get_termination_prover lthy) lthy
   in
     lthy
     |> add pat_completeness_auto |> snd

--- a/src/HOL/Tools/Function/function_common.ML	Sun Oct 21 22:11:38 2012 +0200
+++ b/src/HOL/Tools/Function/function_common.ML	Sun Oct 21 22:12:22 2012 +0200
@@ -44,7 +44,57 @@
 
 end
 
-structure Function_Common =
+signature FUNCTION_COMMON =
+sig
+  include FUNCTION_DATA
+  val profile : bool Unsynchronized.ref
+  val PROFILE : string -> ('a -> 'b) -> 'a -> 'b
+  val mk_acc : typ -> term -> term
+  val function_name : string -> string
+  val graph_name : string -> string
+  val rel_name : string -> string
+  val dom_name : string -> string
+  val apply_termination_rule : Proof.context -> int -> tactic
+  datatype function_result = FunctionResult of
+   {fs: term list,
+    G: term,
+    R: term,
+    psimps : thm list,
+    simple_pinducts : thm list,
+    cases : thm,
+    termination : thm,
+    domintros : thm list option}
+  val transform_function_data : info -> morphism -> info
+  val get_function : Proof.context -> (term * info) Item_Net.T
+  val import_function_data : term -> Proof.context -> info option
+  val import_last_function : Proof.context -> info option
+  val add_function_data : info -> Context.generic -> Context.generic
+  structure Termination_Simps: NAMED_THMS
+  val set_termination_prover : (Proof.context -> tactic) -> Context.generic -> Context.generic
+  val get_termination_prover : Proof.context -> tactic
+  datatype function_config = FunctionConfig of
+   {sequential: bool,
+    default: string option,
+    domintros: bool,
+    partials: bool}
+  val default_config : function_config
+  val split_def : Proof.context -> (string -> 'a) -> term ->
+    string * (string * typ) list * term list * term list * term
+  val check_defs : Proof.context -> ((string * typ) * 'a) list -> term list -> unit
+  type fixes = ((string * typ) * mixfix) list
+  type 'a spec = (Attrib.binding * 'a list) list
+  type preproc = function_config -> Proof.context -> fixes -> term spec ->
+    (term list * (thm list -> thm spec) * (thm list -> thm list list) * string list)
+  val fname_of : term -> string
+  val mk_case_names : int -> string -> int -> string list
+  val empty_preproc : (Proof.context -> ((string * typ) * mixfix) list -> term list -> 'c) -> preproc
+  val get_preproc: Proof.context -> preproc
+  val set_preproc: preproc -> Context.generic -> Context.generic
+  val function_parser : function_config ->
+    ((function_config * (binding * string option * mixfix) list) * (Attrib.binding * string) list) parser
+end
+
+structure Function_Common : FUNCTION_COMMON =
 struct
 
 open Function_Data
@@ -56,7 +106,6 @@
 
 fun PROFILE msg = if !profile then timeap_msg msg else I
 
-
 val acc_const_name = @{const_name accp}
 fun mk_acc domT R =
   Const (acc_const_name, (domT --> domT --> HOLogic.boolT) --> domT --> HOLogic.boolT) $ R 
@@ -179,7 +228,7 @@
 )
 
 val set_termination_prover = TerminationProver.put
-val get_termination_prover = TerminationProver.get o Context.Proof
+fun get_termination_prover ctxt = TerminationProver.get (Context.Proof ctxt) ctxt
 
 
 (* Configuration management *)
@@ -306,7 +355,7 @@
   | mk_case_names _ n 1 = [n]
   | mk_case_names _ n k = map (fn i => n ^ "_" ^ string_of_int i) (1 upto k)
 
-fun empty_preproc check _ ctxt fixes spec =
+fun empty_preproc check (_: function_config) (ctxt: Proof.context) (fixes: fixes) spec =
   let
     val (bnds, tss) = split_list spec
     val ts = flat tss

--- a/src/HOL/Tools/Function/sum_tree.ML	Sun Oct 21 22:11:38 2012 +0200
+++ b/src/HOL/Tools/Function/sum_tree.ML	Sun Oct 21 22:12:22 2012 +0200
@@ -4,7 +4,19 @@
 Some common tools for working with sum types in balanced tree form.
 *)
 
-structure SumTree =
+signature SUM_TREE =
+sig
+  val sumcase_split_ss: simpset
+  val access_top_down: {init: 'a, left: 'a -> 'a, right: 'a -> 'a} -> int -> int -> 'a
+  val mk_sumT: typ -> typ -> typ
+  val mk_sumcase: typ -> typ -> typ -> term -> term -> term
+  val App: term -> term -> term
+  val mk_inj: typ -> int -> int -> term -> term
+  val mk_proj: typ -> int -> int -> term -> term
+  val mk_sumcases: typ -> term list -> term
+end
+
+structure SumTree: SUM_TREE =
 struct
 
 (* Theory dependencies *)
@@ -43,7 +55,7 @@
   |> snd
 
 fun mk_sumcases T fs =
-  Balanced_Tree.make (fn ((f, fT), (g, gT)) => (mk_sumcase fT gT T f g, mk_sumT fT gT)) 
+  Balanced_Tree.make (fn ((f, fT), (g, gT)) => (mk_sumcase fT gT T f g, mk_sumT fT gT))
     (map (fn f => (f, domain_type (fastype_of f))) fs)
   |> fst