provide regular ML interfaces for Isar source language elements;

--- a/src/HOL/Tools/function_package/fundef_datatype.ML	Fri Mar 13 15:50:05 2009 +0100
+++ b/src/HOL/Tools/function_package/fundef_datatype.ML	Fri Mar 13 15:50:06 2009 +0100
@@ -7,11 +7,18 @@
 
 signature FUNDEF_DATATYPE =
 sig
-    val pat_complete_tac: Proof.context -> int -> tactic
+    val pat_completeness_tac: Proof.context -> int -> tactic
+    val pat_completeness: Proof.context -> Proof.method
     val prove_completeness : theory -> term list -> term -> term list list -> term list list -> thm
 
-    val pat_completeness : Proof.context -> method
     val setup : theory -> theory
+
+    val add_fun : FundefCommon.fundef_config ->
+      (binding * typ option * mixfix) list -> (Attrib.binding * term) list ->
+      bool list -> bool -> local_theory -> Proof.context
+    val add_fun_cmd : FundefCommon.fundef_config ->
+      (binding * string option * mixfix) list -> (Attrib.binding * string) list ->
+      bool list -> bool -> local_theory -> Proof.context
 end
 
 structure FundefDatatype : FUNDEF_DATATYPE =
@@ -167,7 +174,7 @@
 
 
 
-fun pat_complete_tac ctxt = SUBGOAL (fn (subgoal, i) =>
+fun pat_completeness_tac ctxt = SUBGOAL (fn (subgoal, i) =>
     let
       val thy = ProofContext.theory_of ctxt
       val (vs, subgf) = dest_all_all subgoal
@@ -196,15 +203,15 @@
     handle COMPLETENESS => no_tac)
 
 
-fun pat_completeness ctxt = Method.SIMPLE_METHOD' (pat_complete_tac ctxt)
+fun pat_completeness ctxt = Method.SIMPLE_METHOD' (pat_completeness_tac ctxt)
 
-val by_pat_completeness_simp =
+val by_pat_completeness_auto =
     Proof.global_future_terminal_proof
       (Method.Basic (pat_completeness, Position.none),
        SOME (Method.Source_i (Args.src (("HOL.auto", []), Position.none))))
 
 fun termination_by method int =
-    FundefPackage.setup_termination_proof NONE
+    FundefPackage.termination_proof NONE
     #> Proof.global_future_terminal_proof
       (Method.Basic (method, Position.none), NONE) int
 
@@ -301,24 +308,28 @@
 val fun_config = FundefConfig { sequential=true, default="%x. undefined" (*FIXME dynamic scoping*), 
                                 domintros=false, tailrec=false }
 
-
-local structure P = OuterParse and K = OuterKeyword in
-
-fun fun_cmd config fixes statements flags int lthy =
+fun gen_fun add config fixes statements flags int lthy =
   let val group = serial_string () in
     lthy
       |> LocalTheory.set_group group
-      |> FundefPackage.add_fundef fixes statements config flags
-      |> by_pat_completeness_simp int
+      |> add fixes statements config flags
+      |> by_pat_completeness_auto int
       |> LocalTheory.restore
       |> LocalTheory.set_group group
-      |> termination_by (FundefCommon.get_termination_prover (Context.Proof lthy)) int
+      |> termination_by (FundefCommon.get_termination_prover lthy) int
   end;
 
+val add_fun = gen_fun FundefPackage.add_fundef
+val add_fun_cmd = gen_fun FundefPackage.add_fundef_cmd
+
+
+
+local structure P = OuterParse and K = OuterKeyword in
+
 val _ =
   OuterSyntax.local_theory' "fun" "define general recursive functions (short version)" K.thy_decl
   (fundef_parser fun_config
-     >> (fn ((config, fixes), (flags, statements)) => fun_cmd config fixes statements flags));
+     >> (fn ((config, fixes), (flags, statements)) => add_fun_cmd config fixes statements flags));
 
 end
 

--- a/src/HOL/Tools/function_package/fundef_package.ML	Fri Mar 13 15:50:05 2009 +0100
+++ b/src/HOL/Tools/function_package/fundef_package.ML	Fri Mar 13 15:50:06 2009 +0100
@@ -7,24 +7,26 @@
 
 signature FUNDEF_PACKAGE =
 sig
-    val add_fundef :  (binding * string option * mixfix) list
+    val add_fundef :  (binding * typ option * mixfix) list
+                       -> (Attrib.binding * term) list
+                       -> FundefCommon.fundef_config
+                       -> bool list
+                       -> local_theory
+                       -> Proof.state
+    val add_fundef_cmd :  (binding * string option * mixfix) list
                       -> (Attrib.binding * string) list 
                       -> FundefCommon.fundef_config
                       -> bool list
                       -> local_theory
                       -> Proof.state
 
-    val add_fundef_i:  (binding * typ option * mixfix) list
-                       -> (Attrib.binding * term) list
-                       -> FundefCommon.fundef_config
-                       -> bool list
-                       -> local_theory
-                       -> Proof.state
-
-    val setup_termination_proof : string option -> 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 : theory -> thm list
+    val get_congs : Proof.context -> thm list
 end
 
 
@@ -114,6 +116,10 @@
         |> Proof.refine (Method.primitive_text (fn _ => goalstate)) |> Seq.hd
     end
 
+val add_fundef = gen_add_fundef false Specification.check_spec (TypeInfer.anyT HOLogic.typeS)
+val add_fundef_cmd = gen_add_fundef true Specification.read_spec "_::type"
+
+
 fun total_termination_afterqed data [[totality]] lthy =
     let
       val FundefCtxData { add_simps, case_names, psimps, pinducts, defname, ... } = data
@@ -136,13 +142,14 @@
         |> note_theorem ((qualify "induct", [Attrib.internal (K (RuleCases.case_names case_names))]), tinduct) |> snd
     end
 
-
-fun setup_termination_proof term_opt lthy =
+fun gen_termination_proof prep_term raw_term_opt lthy =
     let
+      val term_opt = Option.map (prep_term lthy) raw_term_opt
       val data = the (case term_opt of
-                        SOME t => import_fundef_data (Syntax.read_term lthy t) (Context.Proof lthy)
-                      | NONE => import_last_fundef (Context.Proof lthy))
-          handle Option.Option => error ("Not a function: " ^ quote (the_default "" term_opt))
+                        SOME t => (import_fundef_data t lthy
+                          handle Option.Option =>
+                            error ("Not a function: " ^ quote (Syntax.string_of_term lthy t)))
+                      | NONE => (import_last_fundef lthy handle Option.Option => error "Not a function"))
 
         val FundefCtxData {termination, R, ...} = data
         val domT = domain_type (fastype_of R)
@@ -157,13 +164,18 @@
         |> Proof.theorem_i NONE (total_termination_afterqed data) [[(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
+  |> LocalTheory.set_group (serial_string ())
+  |> termination_proof term_opt;
+
 fun termination_cmd term_opt lthy =
   lthy
   |> LocalTheory.set_group (serial_string ())
-  |> setup_termination_proof term_opt;
-
-val add_fundef = gen_add_fundef true Specification.read_spec "_::type"
-val add_fundef_i = gen_add_fundef false Specification.check_spec (TypeInfer.anyT HOLogic.typeS)
+  |> termination_proof_cmd term_opt;
 
 
 (* Datatype hook to declare datatype congs as "fundef_congs" *)
@@ -180,6 +192,7 @@
 
 val setup_case_cong = DatatypePackage.interpretation case_cong
 
+
 (* setup *)
 
 val setup =
@@ -190,7 +203,7 @@
   #> FundefRelation.setup
   #> FundefCommon.TerminationSimps.setup
 
-val get_congs = FundefCtxTree.get_fundef_congs o Context.Theory
+val get_congs = FundefCtxTree.get_fundef_congs
 
 
 (* outer syntax *)
@@ -202,7 +215,7 @@
 val _ =
   OuterSyntax.local_theory_to_proof "function" "define general recursive functions" K.thy_goal
   (fundef_parser default_config
-     >> (fn ((config, fixes), (flags, statements)) => add_fundef fixes statements config flags));
+     >> (fn ((config, fixes), (flags, statements)) => add_fundef_cmd fixes statements config flags));
 
 val _ =
   OuterSyntax.local_theory_to_proof "termination" "prove termination of a recursive function" K.thy_goal

--- a/src/HOL/Tools/function_package/induction_scheme.ML	Fri Mar 13 15:50:05 2009 +0100
+++ b/src/HOL/Tools/function_package/induction_scheme.ML	Fri Mar 13 15:50:06 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Tools/function_package/induction_scheme.ML
-    ID:         $Id$
     Author:     Alexander Krauss, TU Muenchen
 
 A method to prove induction schemes.
@@ -8,7 +7,8 @@
 signature INDUCTION_SCHEME =
 sig
   val mk_ind_tac : (int -> tactic) -> (int -> tactic) -> (int -> tactic)
-                   -> Proof.context -> thm list -> tactic  
+                   -> Proof.context -> thm list -> tactic
+  val induct_scheme_tac : Proof.context -> thm list -> tactic
   val setup : theory -> theory
 end
 
@@ -395,8 +395,11 @@
   end))
 
 
+fun induct_scheme_tac ctxt =
+  mk_ind_tac (K all_tac) (assume_tac APPEND' Goal.assume_rule_tac ctxt) (K all_tac) ctxt;
+
 val setup = Method.add_methods
-  [("induct_scheme", Method.ctxt_args (Method.RAW_METHOD o (fn ctxt => mk_ind_tac (K all_tac) (assume_tac APPEND' Goal.assume_rule_tac ctxt) (K all_tac) ctxt)),
+  [("induct_scheme", Method.ctxt_args (Method.RAW_METHOD o induct_scheme_tac),
     "proves an induction principle")]
 
 end

--- a/src/HOL/Tools/function_package/lexicographic_order.ML	Fri Mar 13 15:50:05 2009 +0100
+++ b/src/HOL/Tools/function_package/lexicographic_order.ML	Fri Mar 13 15:50:06 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:       HOL/Tools/function_package/lexicographic_order.ML
-    ID:          $Id$
     Author:      Lukas Bulwahn, TU Muenchen
 
 Method for termination proofs with lexicographic orderings.
@@ -7,8 +6,9 @@
 
 signature LEXICOGRAPHIC_ORDER =
 sig
-  val lexicographic_order : thm list -> Proof.context -> Method.method
-  val lexicographic_order_tac : Proof.context -> tactic -> tactic
+  val lex_order_tac : Proof.context -> tactic -> tactic
+  val lexicographic_order_tac : Proof.context -> tactic
+  val lexicographic_order : Proof.context -> Proof.method
 
   val setup: theory -> theory
 end
@@ -186,9 +186,10 @@
     end
 
 (** The Main Function **)
-fun lexicographic_order_tac ctxt solve_tac (st: thm) =
+
+fun lex_order_tac ctxt solve_tac (st: thm) =
     let
-      val thy = theory_of_thm st
+      val thy = ProofContext.theory_of ctxt
       val ((trueprop $ (wf $ rel)) :: tl) = prems_of st
 
       val (domT, _) = HOLogic.dest_prodT (HOLogic.dest_setT (fastype_of rel))
@@ -213,12 +214,15 @@
               THEN EVERY (map prove_row clean_table))
     end
 
-fun lexicographic_order thms ctxt = 
-    Method.SIMPLE_METHOD (TRY (FundefCommon.apply_termination_rule ctxt 1)
-                          THEN lexicographic_order_tac ctxt (auto_tac (local_clasimpset_of ctxt addsimps2 FundefCommon.TerminationSimps.get ctxt)))
+fun lexicographic_order_tac ctxt =
+  TRY (FundefCommon.apply_termination_rule ctxt 1)
+  THEN lex_order_tac ctxt (auto_tac (local_clasimpset_of ctxt addsimps2 FundefCommon.TerminationSimps.get ctxt))
+
+val lexicographic_order = Method.SIMPLE_METHOD o lexicographic_order_tac
 
-val setup = Method.add_methods [("lexicographic_order", Method.bang_sectioned_args clasimp_modifiers lexicographic_order,
+val setup = Method.add_methods [("lexicographic_order", Method.only_sectioned_args clasimp_modifiers lexicographic_order,
                                  "termination prover for lexicographic orderings")]
-     #> Context.theory_map (FundefCommon.set_termination_prover (lexicographic_order []))
+     #> Context.theory_map (FundefCommon.set_termination_prover lexicographic_order)
 
-end
+end;
+