replaced "auto_term" by the simpler method "relation", which does not try
to simplify. Some more cleanup.

--- a/src/HOL/FunDef.thy	Mon Nov 13 12:10:49 2006 +0100
+++ b/src/HOL/FunDef.thy	Mon Nov 13 13:51:22 2006 +0100
@@ -199,11 +199,10 @@
 use "Tools/function_package/termination.ML"
 use "Tools/function_package/mutual.ML"
 use "Tools/function_package/pattern_split.ML"
+use "Tools/function_package/auto_term.ML"
 use "Tools/function_package/fundef_package.ML"
-use "Tools/function_package/auto_term.ML"
 
 setup FundefPackage.setup
-setup FundefAutoTerm.setup
 
 lemmas [fundef_cong] = 
   let_cong if_cong image_cong INT_cong UN_cong bex_cong ball_cong imp_cong

--- a/src/HOL/Tools/function_package/auto_term.ML	Mon Nov 13 12:10:49 2006 +0100
+++ b/src/HOL/Tools/function_package/auto_term.ML	Mon Nov 13 13:51:22 2006 +0100
@@ -3,48 +3,37 @@
     Author:     Alexander Krauss, TU Muenchen
 
 A package for general recursive function definitions.
-The auto_term method.
+Method "relation" to commence a termination proof using a user-specified relation.
 *)
 
 
-signature FUNDEF_AUTO_TERM =
+signature FUNDEF_RELATION =
 sig
+  val relation_meth : Proof.context -> term -> Method.method
+
   val setup: theory -> theory
 end
 
-structure FundefAutoTerm : FUNDEF_AUTO_TERM =
+structure FundefRelation : FUNDEF_RELATION =
 struct
 
-open FundefCommon
-open FundefAbbrev
-
-
-fun auto_term_tac ctxt rule rel wf_rules ss =
-  let
-    val cert = Thm.cterm_of (ProofContext.theory_of ctxt)
-
-    val rel' = cert (singleton (Variable.polymorphic ctxt) rel)
-    val rule' = rule |> Thm.incr_indexes (#maxidx (Thm.rep_cterm rel') + 1)
-    val prem = #1 (Logic.dest_implies (Thm.prop_of rule'))
-    val R' = cert (Var (the_single (Term.add_vars prem [])))
-  in
-    rtac (Drule.cterm_instantiate [(R', rel')] rule') 1  (* instantiate termination rule *)
-    THEN (ALLGOALS
-      (fn 1 => REPEAT (ares_tac wf_rules 1)    (* Solve wellfoundedness *)
-        | i => asm_simp_tac ss i))             (* Simplify termination conditions *)
-  end
-
-
-fun termination_meth src = Method.syntax Args.term src #> (fn (ctxt, rel) =>
-  let
-    val {simps, congs, wfs} = RecdefPackage.get_hints (Context.Proof ctxt)
-    val ss = local_simpset_of ctxt addsimps simps
-
-    val intro_rule = ProofContext.get_thm ctxt (Name "termination")
-    (* FIXME avoid internal name lookup -- dynamic scoping! *)
-  in Method.SIMPLE_METHOD (auto_term_tac ctxt intro_rule rel wfs ss) end)
+fun relation_meth ctxt rel = 
+    let
+      val cert = Thm.cterm_of (ProofContext.theory_of ctxt)
+                 
+      val rel' = cert (singleton (Variable.polymorphic ctxt) rel)
+      val rule = FundefCommon.get_termination_rule ctxt |> the
+                  |> Thm.incr_indexes (#maxidx (Thm.rep_cterm rel') + 1)
+          
+      val prem = #1 (Logic.dest_implies (Thm.prop_of rule))
+      val Rvar = cert (Var (the_single (Term.add_vars prem [])))
+    in
+      Method.SIMPLE_METHOD (rtac (Drule.cterm_instantiate [(Rvar, rel')] rule) 1)
+    end
+   
 
 val setup = Method.add_methods
-  [("auto_term", termination_meth, "proves termination using a user-specified wellfounded relation")]
+  [("relation", uncurry relation_meth oo Method.syntax Args.term,
+    "proves termination using a user-specified wellfounded relation")]
 
 end

--- a/src/HOL/Tools/function_package/fundef_common.ML	Mon Nov 13 12:10:49 2006 +0100
+++ b/src/HOL/Tools/function_package/fundef_common.ML	Mon Nov 13 13:51:22 2006 +0100
@@ -20,6 +20,12 @@
 fun mk_acc domT R =
     Const (acc_const_name, (fastype_of R) --> domT --> HOLogic.boolT) $ R 
 
+val function_name = suffix "C"
+val graph_name = suffix "_graph"
+val rel_name = suffix "_rel"
+val dom_name = suffix "_dom"
+
+val dest_rel_name = unsuffix "_rel"
 
 type depgraph = int IntGraph.T
 
@@ -216,8 +222,7 @@
     type T = thm list
     val empty = []
     val extend = I
-    fun merge _ (l1, l2) = l1 @ l2
-      (* FIXME exponential blowup! cf. Library.merge, Drule.merge_rules *)
+    fun merge _ = Drule.merge_rules
     fun print  _ _ = ()
 end);
 
@@ -230,16 +235,32 @@
 fun set_last_fundef name = FundefData.map (apfst (K name))
 fun get_last_fundef thy = fst (FundefData.get thy)
 
+
 val map_fundef_congs = FundefCongs.map 
 val get_fundef_congs = FundefCongs.get
 
 
+
+structure TerminationRule = ProofDataFun
+(struct
+    val name = "HOL/function_def/termination"
+    type T = thm option
+    val init = K NONE
+    fun print  _ _ = ()
+end);
+
+val get_termination_rule = TerminationRule.get 
+val set_termination_rule = TerminationRule.map o K o SOME
+
+
+
 (* Configuration management *)
 datatype fundef_opt 
   = Sequential
   | Default of string
   | Preprocessor of string
   | Target of xstring
+  | DomIntros
 
 datatype fundef_config
   = FundefConfig of
@@ -247,21 +268,24 @@
     sequential: bool,
     default: string,
     preprocessor: string option,
-    target: xstring option
+    target: xstring option,
+    domintros: bool
    }
 
 
-val default_config = FundefConfig { sequential=false, default="%x. arbitrary", preprocessor=NONE, target=NONE }
-val fun_config = FundefConfig { sequential=true, default="%x. arbitrary", preprocessor=NONE, target=NONE }
+val default_config = FundefConfig { sequential=false, default="%x. arbitrary", preprocessor=NONE, target=NONE, domintros=false }
+val fun_config = FundefConfig { sequential=true, default="%x. arbitrary", preprocessor=NONE, target=NONE, domintros=false }
 
-fun apply_opt Sequential (FundefConfig {sequential, default, preprocessor, target}) = 
-    FundefConfig {sequential=true, default=default, preprocessor=preprocessor, target=target }
-  | apply_opt (Default d) (FundefConfig {sequential, default, preprocessor, target}) = 
-    FundefConfig {sequential=sequential, default=d, preprocessor=preprocessor, target=target }
-  | apply_opt (Preprocessor p) (FundefConfig {sequential, default, preprocessor, target}) = 
-    FundefConfig {sequential=sequential, default=default, preprocessor=SOME p, target=target }
-  | apply_opt (Target t) (FundefConfig {sequential, default, preprocessor, target }) =
-    FundefConfig {sequential=sequential, default=default, preprocessor=preprocessor, target=SOME t }
+fun apply_opt Sequential (FundefConfig {sequential, default, preprocessor, target, domintros}) = 
+    FundefConfig {sequential=true, default=default, preprocessor=preprocessor, target=target, domintros=domintros }
+  | apply_opt (Default d) (FundefConfig {sequential, default, preprocessor, target, domintros}) = 
+    FundefConfig {sequential=sequential, default=d, preprocessor=preprocessor, target=target, domintros=domintros }
+  | apply_opt (Preprocessor p) (FundefConfig {sequential, default, preprocessor, target, domintros}) = 
+    FundefConfig {sequential=sequential, default=default, preprocessor=SOME p, target=target, domintros=domintros }
+  | apply_opt (Target t) (FundefConfig {sequential, default, preprocessor, target, domintros }) =
+    FundefConfig {sequential=sequential, default=default, preprocessor=preprocessor, target=SOME t, domintros=domintros }
+  | apply_opt Domintros (FundefConfig {sequential, default, preprocessor, target, domintros }) =
+    FundefConfig {sequential=sequential, default=default, preprocessor=preprocessor, target=target, domintros=true }
 
 
 local structure P = OuterParse and K = OuterKeyword in
@@ -270,6 +294,7 @@
 
 val option_parser = (P.$$$ "sequential" >> K Sequential)
                || ((P.reserved "default" |-- P.term) >> Default)
+               || (P.reserved "domintros" >> K DomIntros)
                || ((P.$$$ "in" |-- P.xname) >> Target)
 
 fun config_parser def = (Scan.optional (P.$$$ "(" |-- P.list1 option_parser --| P.$$$ ")") [])
@@ -287,6 +312,12 @@
 
 
 
+
+
+
+
+
+
 end
 
 

--- a/src/HOL/Tools/function_package/fundef_datatype.ML	Mon Nov 13 12:10:49 2006 +0100
+++ b/src/HOL/Tools/function_package/fundef_datatype.ML	Mon Nov 13 13:51:22 2006 +0100
@@ -171,7 +171,7 @@
 
 fun termination_by_lexicographic_order name =
     FundefPackage.setup_termination_proof (SOME name)
-    #> Proof.global_terminal_proof (Method.Basic (K LexicographicOrder.lexicographic_order), NONE)
+    #> Proof.global_terminal_proof (Method.Basic LexicographicOrder.lexicographic_order, NONE)
 
 val setup =
     Method.add_methods [("pat_completeness", Method.no_args pat_completeness, "Completeness prover for datatype patterns")]

--- a/src/HOL/Tools/function_package/fundef_lib.ML	Mon Nov 13 12:10:49 2006 +0100
+++ b/src/HOL/Tools/function_package/fundef_lib.ML	Mon Nov 13 13:51:22 2006 +0100
@@ -10,6 +10,9 @@
 
 structure FundefLib = struct
 
+fun plural sg pl [x] = sg
+  | plural sg pl _ = pl
+
 fun eq_str (s : string, t) = (s = t) (* monomorphic equality on strings *)
 
 fun mk_forall v t = all (fastype_of v) $ lambda v t
@@ -36,14 +39,15 @@
 (* Removes all quantifiers from a term, replacing bound variables by frees. *)
 fun dest_all_all (t as (Const ("all",_) $ _)) = 
     let
-  val (v,b) = dest_all t
-  val (vs, b') = dest_all_all b
+      val (v,b) = dest_all t
+      val (vs, b') = dest_all_all b
     in
-  (v :: vs, b')
+      (v :: vs, b')
     end
   | dest_all_all t = ([],t)
+                     
 
-
+(* FIXME: similar to Variable.focus *)
 fun dest_all_all_ctx ctx (Const ("all", _) $ Abs (a as (n,T,b))) =
     let
       val [(n', _)] = Variable.variant_frees ctx [] [(n,T)]
@@ -87,12 +91,18 @@
 
 (* Replaces Frees by name. Probably quicker than Pattern.rewrite_terms, and works with loose Bounds. *)
 fun replace_frees assoc =
-    map_aterms (fn c as Free (n, _) => (case AList.lookup (op =) assoc n of
-                                          NONE => c
-                                        | SOME t => t)
+    map_aterms (fn c as Free (n, _) => the_default c (AList.lookup (op =) assoc n)
                  | t => t)
 
 
+fun forall_aterms P (t $ u) = forall_aterms P t andalso forall_aterms P u
+  | forall_aterms P (Abs (_, _, t)) = forall_aterms P t
+  | forall_aterms P a = P a
+
+fun exists_aterm P = not o forall_aterms (not o P)
+
+
+
 
 fun rename_bound n (Q $ Abs(_, T, b)) = (Q $ Abs(n, T, b))
   | rename_bound n _ = raise Match
@@ -100,27 +110,27 @@
 fun mk_forall_rename (n, v) =
     rename_bound n o mk_forall v 
 
+val dummy_term = Free ("", dummyT)
+
 fun forall_intr_rename (n, cv) thm =
     let
       val allthm = forall_intr cv thm
-      val reflx = prop_of allthm
-                   |> rename_bound n
-                   |> cterm_of (theory_of_thm thm)
-                   |> reflexive
+      val (_, abs) = Logic.dest_all (prop_of allthm)
     in
-      equal_elim reflx allthm
+      Thm.rename_boundvars abs (Abs (n, dummyT, dummy_term)) allthm
     end
 
 
 (* Returns the frees in a term in canonical order, excluding the fixes from the context *)
 fun frees_in_term ctxt t =
+    Term.add_frees t []
+    |> filter_out (Variable.is_fixed ctxt o fst)
+    |> rev
+(*
     rev (fold_aterms (fn  Free (v as (x, _)) =>
                           if Variable.is_fixed ctxt x then I else insert (fn ((x, _),(y, _)) => x = y) v | _ => I) t [])
-
+*)
 
-fun plural sg pl [] = sys_error "plural"
-  | plural sg pl [x] = sg
-  | plural sg pl (x::y::ys) = pl
 
 
 end
\ No newline at end of file

--- a/src/HOL/Tools/function_package/fundef_package.ML	Mon Nov 13 12:10:49 2006 +0100
+++ b/src/HOL/Tools/function_package/fundef_package.ML	Mon Nov 13 13:51:22 2006 +0100
@@ -38,8 +38,6 @@
 open FundefLib
 open FundefCommon
 
-(*fn (ctxt,s) => Variable.importT_terms (fst (ProofContext.read_termTs ctxt (K false) (K NONE) (K NONE) [] [s])) ctxt;*)
-
 fun burrow_snd f ps = (* ('a list -> 'b list) -> ('c * 'a) list -> ('c * 'b) list *)
     let val (xs, ys) = split_list ps
     in xs ~~ f ys end
@@ -64,8 +62,9 @@
     end
 
 
-fun fundef_afterqed fixes spec mutual_info defname data [[result]] lthy =
+fun fundef_afterqed config fixes spec mutual_info defname data [[result]] lthy =
     let
+      val FundefConfig { domintros, ...} = config
       val Prep {f, R, ...} = data
       val fundef_data = FundefMutual.mk_partial_rules_mutual lthy mutual_info data result
       val FundefMResult {psimps, subset_pinducts, simple_pinducts, termination, domintros, cases, ...} = fundef_data
@@ -119,7 +118,7 @@
       val ((mutual_info, name, prep_result as Prep {goal, goalI, ...}), lthy) =
           FundefMutual.prepare_fundef_mutual fixes t_eqns default lthy
 
-      val afterqed = fundef_afterqed fixes spec mutual_info name prep_result
+      val afterqed = fundef_afterqed config fixes spec mutual_info name prep_result
     in
       (name, lthy
          |> Proof.theorem_i PureThy.internalK NONE afterqed NONE ("", []) [(("", []), [(goal, [])])]
@@ -162,6 +161,7 @@
       lthy
         |> ProofContext.note_thmss_i [(("termination",
                                         [ContextRules.intro_query NONE]), [(ProofContext.standard lthy [termination], [])])] |> snd
+        |> set_termination_rule termination
         |> Proof.theorem_i PureThy.internalK NONE
                            (total_termination_afterqed name data) NONE ("", [])
                            [(("", []), [(goal, [])])]
@@ -199,9 +199,11 @@
 val setup = 
     FundefData.init 
       #> FundefCongs.init
+      #> TerminationRule.init
       #>  Attrib.add_attributes
             [("fundef_cong", Attrib.add_del_args cong_add cong_del, "declaration of congruence rule for function definitions")]
       #> setup_case_cong_hook
+      #> FundefRelation.setup
 
 val get_congs = FundefCommon.get_fundef_congs o Context.Theory
 

--- a/src/HOL/Tools/function_package/fundef_prep.ML	Mon Nov 13 12:10:49 2006 +0100
+++ b/src/HOL/Tools/function_package/fundef_prep.ML	Mon Nov 13 13:51:22 2006 +0100
@@ -188,31 +188,31 @@
 (* if j < i, then turn around *)
 fun get_compat_thm thy cts i j ctxi ctxj = 
     let
-        val ClauseContext {cqs=cqsi,ags=agsi,lhs=lhsi,...} = ctxi
-        val ClauseContext {cqs=cqsj,ags=agsj,lhs=lhsj,...} = ctxj
-
-        val lhsi_eq_lhsj = cterm_of thy (Trueprop (mk_eq (lhsi, lhsj)))
+      val ClauseContext {cqs=cqsi,ags=agsi,lhs=lhsi,...} = ctxi
+      val ClauseContext {cqs=cqsj,ags=agsj,lhs=lhsj,...} = ctxj
+          
+      val lhsi_eq_lhsj = cterm_of thy (Trueprop (mk_eq (lhsi, lhsj)))
     in if j < i then
-           let
-               val compat = lookup_compat_thm j i cts
-           in
-               compat         (* "!!qj qi. Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *)
+         let
+           val compat = lookup_compat_thm j i cts
+         in
+           compat         (* "!!qj qi. Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *)
                 |> fold forall_elim (cqsj @ cqsi) (* "Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *)
                 |> fold implies_elim_swp agsj
                 |> fold implies_elim_swp agsi
                 |> implies_elim_swp ((assume lhsi_eq_lhsj) RS sym) (* "Gsj, Gsi, lhsi = lhsj |-- rhsj = rhsi" *)
-           end
+         end
        else
-           let
-               val compat = lookup_compat_thm i j cts
-           in
+         let
+           val compat = lookup_compat_thm i j cts
+         in
                compat        (* "!!qi qj. Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *)
                  |> fold forall_elim (cqsi @ cqsj) (* "Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *)
                  |> fold implies_elim_swp agsi
                  |> fold implies_elim_swp agsj
                  |> implies_elim_swp (assume lhsi_eq_lhsj)
                  |> (fn thm => thm RS sym) (* "Gsi, Gsj, lhsi = lhsj |-- rhsj = rhsi" *)
-           end
+         end
     end
 
 
@@ -237,6 +237,7 @@
                                 |> fold_rev (implies_intr o cprop_of) h_assums
                                 |> fold_rev (implies_intr o cprop_of) ags
                                 |> fold_rev forall_intr cqs
+                                |> Drule.close_derivation
     in
       replace_lemma
     end
@@ -364,7 +365,6 @@
                                   |> forall_intr (cterm_of thy x)
                                   |> (fn it => Drule.compose_single (it, 2, acc_induct_rule)) (* "EX! y. (?x,y):G" *)
                                   |> (fn it => fold (forall_intr o cterm_of thy) (term_vars (prop_of it)) it)
-                                  |> Drule.close_derivation
 
         val goal = complete COMP (graph_is_function COMP conjunctionI)
                             |> Drule.close_derivation
@@ -477,8 +477,6 @@
       val fvar = Free (fname, fT)
       val domT = domain_type fT
       val ranT = range_type fT
-
-                 
                             
       val [default] = fst (Variable.importT_terms (fst (ProofContext.read_termTs lthy (K false) (K NONE) (K NONE) [] [(default_str, fT)])) lthy) (* FIXME *)
 
@@ -499,14 +497,14 @@
       val trees = PROFILE "making trees" (map build_tree) clauses
       val RCss = PROFILE "finding calls" (map find_calls) trees
 
-      val ((G, GIntro_thms, G_elim), lthy) = PROFILE "def_graph" (define_graph (defname ^ "_graph") fvar domT ranT clauses RCss) lthy
+      val ((G, GIntro_thms, G_elim), lthy) = PROFILE "def_graph" (define_graph (graph_name defname) fvar domT ranT clauses RCss) lthy
       val ((f, f_defthm), lthy) = PROFILE "def_fun" (define_function (defname ^ "_sum_def") (fname, mixfix) domT ranT G default) lthy
 
       val RCss = PROFILE "inst_RCs" (map (map (inst_RC (ProofContext.theory_of lthy) fvar f))) RCss
       val trees = PROFILE "inst_trees" (map (FundefCtxTree.inst_tree (ProofContext.theory_of lthy) fvar f)) trees
 
       val ((R, RIntro_thmss, R_elim), lthy) = 
-          PROFILE "def_rel" (define_recursion_relation (defname ^ "_rel") domT ranT fvar f abstract_qglrs clauses RCss) lthy
+          PROFILE "def_rel" (define_recursion_relation (rel_name defname) domT ranT fvar f abstract_qglrs clauses RCss) lthy
 
       val lthy = PROFILE "abbrev"
         (snd o LocalTheory.abbrevs ("", false) (* FIXME really this mode? cf. Syntax.default_mode *)

--- a/src/HOL/Tools/function_package/lexicographic_order.ML	Mon Nov 13 12:10:49 2006 +0100
+++ b/src/HOL/Tools/function_package/lexicographic_order.ML	Mon Nov 13 13:51:22 2006 +0100
@@ -7,7 +7,7 @@
 
 signature LEXICOGRAPHIC_ORDER =
 sig
-  val lexicographic_order : Method.method
+  val lexicographic_order : Proof.context -> Method.method
   val setup: theory -> theory
 end
 
@@ -201,10 +201,10 @@
       
 (* the main function: create table, search table, create relation,
    and prove the subgoals *)
-fun lexicographic_order_tac (st: thm) = 
+fun lexicographic_order_tac ctxt (st: thm) = 
     let
       val thy = theory_of_thm st
-      val termination_thm = ProofContext.get_thm (Variable.thm_context st) (Name "termination")
+      val termination_thm = the (FundefCommon.get_termination_rule ctxt)
       val next_st = SINGLE (rtac termination_thm 1) st |> the
       val premlist = prems_of next_st
     in
@@ -239,8 +239,8 @@
             end
     end
 
-val lexicographic_order = Method.SIMPLE_METHOD lexicographic_order_tac
+val lexicographic_order = Method.SIMPLE_METHOD o lexicographic_order_tac
 
-val setup = Method.add_methods [("lexicographic_order", Method.no_args lexicographic_order, "termination prover for lexicographic orderings")]
+val setup = Method.add_methods [("lexicographic_order", Method.ctxt_args lexicographic_order, "termination prover for lexicographic orderings")]
 
 end
\ No newline at end of file

--- a/src/HOL/Tools/function_package/mutual.ML	Mon Nov 13 12:10:49 2006 +0100
+++ b/src/HOL/Tools/function_package/mutual.ML	Mon Nov 13 13:51:22 2006 +0100
@@ -49,7 +49,7 @@
 (* Builds a curried clause description in abstracted form *)
 fun split_def ctxt fnames geq arities =
     let
-      fun input_error msg = error (cat_lines [msg, ProofContext.string_of_term ctxt geq])
+      fun input_error msg = cat_lines [msg, ProofContext.string_of_term ctxt geq]
                             
       val (qs, imp) = open_all_all geq
 
@@ -61,32 +61,27 @@
 
       val invalid_head_msg = "Head symbol of left hand side must be " ^ plural "" "one out of " fnames ^ commas_quote fnames
       val fname = fst (dest_Free head)
-          handle TERM _ => input_error invalid_head_msg
+          handle TERM _ => error (input_error invalid_head_msg)
 
-      val _ = if fname mem fnames then ()
-              else input_error invalid_head_msg
+      val _ = assert (fname mem fnames) (input_error invalid_head_msg)
 
       fun add_bvs t is = add_loose_bnos (t, 0, is)
       val rvs = (add_bvs rhs [] \\ fold add_bvs args [])
                   |> map (fst o nth (rev qs))
                 
-      val _ = if null rvs then ()
-              else input_error ("Variable" ^ plural " " "s " rvs ^ commas_quote rvs
-                                ^ " occur" ^ plural "s" "" rvs ^ " on right hand side only:")
+      val _ = assert (null rvs) (input_error ("Variable" ^ plural " " "s " rvs ^ commas_quote rvs
+                                              ^ " occur" ^ plural "s" "" rvs ^ " on right hand side only:"))
 
-      val _ = (fold o fold_aterms)
-                 (fn Free (n, _) => if n mem fnames
-                                    then input_error "Recursive Calls not allowed in premises:"
-                                    else I
-                   | _ => I) gs ()
+      val _ = assert (forall (forall_aterms (fn Free (n, _) => not (n mem fnames) | _ => true)) gs)
+                     (input_error "Recursive Calls not allowed in premises")
 
       val k = length args
 
       val arities' = case Symtab.lookup arities fname of
                        NONE => Symtab.update (fname, k) arities
-                     | SOME i => if (i <> k)
-                                 then input_error ("Function " ^ quote fname ^ " has different numbers of arguments in different equations")
-                                 else arities
+                     | SOME i => (assert (i = k)
+                                  (input_error ("Function " ^ quote fname ^ " has different numbers of arguments in different equations"));
+                                  arities)
     in
       ((fname, qs, gs, args, rhs), arities')
     end

--- a/src/HOL/ex/CodeCollections.thy	Mon Nov 13 12:10:49 2006 +0100
+++ b/src/HOL/ex/CodeCollections.thy	Mon Nov 13 13:51:22 2006 +0100
@@ -72,8 +72,6 @@
 | "abs_sorted cmp [x] = True"
 | "abs_sorted cmp (x#y#xs) = (cmp x y \<and> abs_sorted cmp (y#xs))"
 
-termination by (auto_term "measure (length o snd)")
-
 thm abs_sorted.simps
 
 abbreviation (in ordered)
@@ -117,8 +115,6 @@
 | "le_option' (Some x) None = False"
 | "le_option' (Some x) (Some y) = x <<= y"
 
-termination by (auto_term "{}")
-
 instance option :: (ordered) ordered
   "x <<= y == le_option' x y"
 proof (default, unfold ordered_option_def)
@@ -147,7 +143,6 @@
 fun le_pair' :: "'a::ordered \<times> 'b::ordered \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
 where
   "le_pair' (x1, y1) (x2, y2) = (x1 << x2 \<or> x1 = x2 \<and> y1 <<= y2)"
-termination by (auto_term "{}")
 
 instance * :: (ordered, ordered) ordered
   "x <<= y == le_pair' x y"
@@ -169,8 +164,6 @@
 | "le_list' (x#xs) [] = False"
 | "le_list' (x#xs) (y#ys) = (x << y \<or> x = y \<and> le_list' xs ys)"
 
-termination by (auto_term "measure (length o fst)")
-
 instance (ordered) list :: ordered
   "xs <<= ys == le_list' xs ys"
 proof (default, unfold "ordered_list_def")

--- a/src/HOL/ex/Codegenerator.thy	Mon Nov 13 12:10:49 2006 +0100
+++ b/src/HOL/ex/Codegenerator.thy	Mon Nov 13 13:51:22 2006 +0100
@@ -48,7 +48,7 @@
   fac :: "int => int" where
   "fac j = (if j <= 0 then 1 else j * (fac (j - 1)))"
   by pat_completeness auto
-termination by (auto_term "measure nat")
+termination by (relation "measure nat") auto
 
 declare fac.simps [code]
 

--- a/src/HOL/ex/Fundefs.thy	Mon Nov 13 12:10:49 2006 +0100
+++ b/src/HOL/ex/Fundefs.thy	Mon Nov 13 13:51:22 2006 +0100
@@ -17,8 +17,7 @@
 | "fib (Suc 0) = 1"
 | "fib (Suc (Suc n)) = fib n + fib (Suc n)"
 
-
-text {* we get partial simp and induction rules: *}
+text {* partial simp and induction rules: *}
 thm fib.psimps
 thm fib.pinduct
 
@@ -27,15 +26,10 @@
 
 thm fib.domintros
 
-
-text {* Now termination: *}
-(*termination fib
-  by (auto_term "less_than")*)
-
+text {* total simp and induction rules: *}
 thm fib.simps
 thm fib.induct
 
-
 section {* Currying *}
 
 fun add :: "nat \<Rightarrow> nat \<Rightarrow> nat"
@@ -62,8 +56,7 @@
 by induct auto
 
 termination nz
-  apply (auto_term "less_than") -- {* Oops, it left us something to prove *}
-  by (auto simp:nz_is_zero)
+  by (relation "less_than") (auto simp:nz_is_zero)
 
 thm nz.simps
 thm nz.induct