# HG changeset patch # User krauss # Date 1180790918 -7200 # Node ID a5026e73cfcf374413b2bd9865e3b71321d4d78b # Parent 98736a2fec98d5c99b9135e2500d104e2ed4b012 "function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases. more cleanup. diff -r 98736a2fec98 -r a5026e73cfcf src/HOL/FunDef.thy --- a/src/HOL/FunDef.thy Sat Jun 02 15:26:32 2007 +0200 +++ b/src/HOL/FunDef.thy Sat Jun 02 15:28:38 2007 +0200 @@ -9,8 +9,8 @@ imports Datatype Accessible_Part uses ("Tools/function_package/sum_tools.ML") + ("Tools/function_package/fundef_lib.ML") ("Tools/function_package/fundef_common.ML") - ("Tools/function_package/fundef_lib.ML") ("Tools/function_package/inductive_wrap.ML") ("Tools/function_package/context_tree.ML") ("Tools/function_package/fundef_core.ML") @@ -88,8 +88,8 @@ use "Tools/function_package/sum_tools.ML" +use "Tools/function_package/fundef_lib.ML" use "Tools/function_package/fundef_common.ML" -use "Tools/function_package/fundef_lib.ML" use "Tools/function_package/inductive_wrap.ML" use "Tools/function_package/context_tree.ML" use "Tools/function_package/fundef_core.ML" diff -r 98736a2fec98 -r a5026e73cfcf src/HOL/Tools/function_package/fundef_common.ML --- a/src/HOL/Tools/function_package/fundef_common.ML Sat Jun 02 15:26:32 2007 +0200 +++ b/src/HOL/Tools/function_package/fundef_common.ML Sat Jun 02 15:28:38 2007 +0200 @@ -3,7 +3,7 @@ Author: Alexander Krauss, TU Muenchen A package for general recursive function definitions. -Common type definitions and other infrastructure. +Common definitions and other infrastructure. *) structure FundefCommon = @@ -153,12 +153,10 @@ #> store_termination_rule termination - (* Configuration management *) datatype fundef_opt = Sequential | Default of string - | Preprocessor of string | Target of xstring | DomIntros | Tailrec @@ -168,64 +166,24 @@ { sequential: bool, default: string, - preprocessor: string option, target: xstring option, domintros: bool, tailrec: bool } - -val default_config = FundefConfig { sequential=false, default="%x. arbitrary", preprocessor=NONE, - target=NONE, domintros=false, tailrec=false } - -val fun_config = FundefConfig { sequential=true, default="%x. arbitrary", preprocessor=NONE, - target=NONE, domintros=false, tailrec=false } - -fun apply_opt Sequential (FundefConfig {sequential, default, preprocessor, target, domintros,tailrec}) = - FundefConfig {sequential=true, default=default, preprocessor=preprocessor, target=target, domintros=domintros, tailrec=tailrec } - | apply_opt (Default d) (FundefConfig {sequential, default, preprocessor, target, domintros,tailrec}) = - FundefConfig {sequential=sequential, default=d, preprocessor=preprocessor, target=target, domintros=domintros, tailrec=tailrec } - | apply_opt (Preprocessor p) (FundefConfig {sequential, default, preprocessor, target, domintros,tailrec}) = - FundefConfig {sequential=sequential, default=default, preprocessor=SOME p, target=target, domintros=domintros, tailrec=tailrec } - | apply_opt (Target t) (FundefConfig {sequential, default, preprocessor, target, domintros,tailrec }) = - FundefConfig {sequential=sequential, default=default, preprocessor=preprocessor, target=SOME t, domintros=domintros, tailrec=tailrec } - | apply_opt DomIntros (FundefConfig {sequential, default, preprocessor, target, domintros,tailrec }) = - FundefConfig {sequential=sequential, default=default, preprocessor=preprocessor, target=target, domintros=true,tailrec=tailrec } - | apply_opt Tailrec (FundefConfig {sequential, default, preprocessor, target, domintros,tailrec }) = - FundefConfig {sequential=sequential, default=default, preprocessor=preprocessor, target=target, domintros=domintros,tailrec=true } +fun apply_opt Sequential (FundefConfig {sequential, default, target, domintros,tailrec}) = + FundefConfig {sequential=true, default=default, target=target, domintros=domintros, tailrec=tailrec} + | apply_opt (Default d) (FundefConfig {sequential, default, target, domintros,tailrec}) = + FundefConfig {sequential=sequential, default=d, target=target, domintros=domintros, tailrec=tailrec} + | apply_opt (Target t) (FundefConfig {sequential, default, target, domintros,tailrec}) = + FundefConfig {sequential=sequential, default=default, target=SOME t, domintros=domintros, tailrec=tailrec} + | apply_opt DomIntros (FundefConfig {sequential, default, target, domintros,tailrec}) = + FundefConfig {sequential=sequential, default=default, target=target, domintros=true,tailrec=tailrec} + | apply_opt Tailrec (FundefConfig {sequential, default, target, domintros,tailrec}) = + FundefConfig {sequential=sequential, default=default, target=target, domintros=domintros,tailrec=true} fun target_of (FundefConfig {target, ...}) = target -local - structure P = OuterParse and K = OuterKeyword - - val opt_sequential = Scan.optional ((P.$$$ "(" |-- P.$$$ "sequential" --| P.$$$ ")") >> K true) false - - val option_parser = (P.$$$ "sequential" >> K Sequential) - || ((P.reserved "default" |-- P.term) >> Default) - || (P.reserved "domintros" >> K DomIntros) - || (P.reserved "tailrec" >> K Tailrec) - || ((P.$$$ "in" |-- P.xname) >> Target) - - fun config_parser def = (Scan.optional (P.$$$ "(" |-- P.!!! (P.list1 (P.group "option" option_parser)) --| P.$$$ ")") []) - >> (fn opts => fold apply_opt opts def) - - fun pipe_list1 s = P.enum1 "|" s - - val otherwise = P.$$$ "(" |-- P.$$$ "otherwise" --| P.$$$ ")" - - fun pipe_error t = P.!!! (Scan.fail_with (K (cat_lines ["Equations must be separated by " ^ quote "|", quote t]))) - - val statement_ow = SpecParse.opt_thm_name ":" -- (P.prop -- Scan.optional (otherwise >> K true) false) - --| Scan.ahead ((P.term :-- pipe_error) || Scan.succeed ("","")) - - val statements_ow = pipe_list1 statement_ow -in - fun fundef_parser default_cfg = config_parser default_cfg -- P.fixes --| P.$$$ "where" -- statements_ow -end - - - (* Common operations on equations *) fun open_all_all (Const ("all", _) $ Abs (n, T, b)) = apfst (cons (n, T)) (open_all_all b) @@ -266,6 +224,106 @@ end +(* Check for all sorts of errors in the input *) +fun check_defs ctxt fixes eqs = + let + val fnames = map (fst o fst) fixes + + fun check geq = + let + fun input_error msg = cat_lines [msg, ProofContext.string_of_term ctxt geq] + + val fqgar as (fname, qs, gs, args, rhs) = split_def geq + + val _ = fname mem fnames + orelse error (input_error ("Head symbol of left hand side must be " ^ plural "" "one out of " fnames + ^ commas_quote fnames)) + + 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 _ = null rvs orelse error (input_error ("Variable" ^ plural " " "s " rvs ^ commas_quote rvs + ^ " occur" ^ plural "s" "" rvs ^ " on right hand side only:")) + + val _ = forall (FundefLib.forall_aterms (fn Free (n, _) => not (n mem fnames) | _ => true)) gs + orelse error (input_error "Recursive Calls not allowed in premises") + in + fqgar + end + + val _ = mk_arities (map check eqs) + handle ArgumentCount fname => + error ("Function " ^ quote fname ^ " has different numbers of arguments in different equations") + in + () + end + +(* Preprocessors *) + +type fixes = ((string * typ) * mixfix) list +type 'a spec = ((bstring * Attrib.src list) * 'a list) list +type preproc = fundef_config -> bool list -> Proof.context -> fixes -> term spec -> (term list * (thm list -> thm spec)) + +fun empty_preproc check _ _ ctxt fixes spec = + let + val (nas,tss) = split_list spec + val _ = check ctxt fixes (flat tss) + in + (flat tss, curry op ~~ nas o Library.unflat tss) + end + +structure Preprocessor = GenericDataFun +( + type T = preproc + val empty = empty_preproc check_defs + val extend = I + fun merge _ (a, _) = a +); + +val get_preproc = Preprocessor.get o Context.Proof +val set_preproc = Preprocessor.map o K + + + +local + structure P = OuterParse and K = OuterKeyword + + val opt_sequential = Scan.optional ((P.$$$ "(" |-- P.$$$ "sequential" --| P.$$$ ")") >> K true) false + + val option_parser = (P.$$$ "sequential" >> K Sequential) + || ((P.reserved "default" |-- P.term) >> Default) + || (P.reserved "domintros" >> K DomIntros) + || (P.reserved "tailrec" >> K Tailrec) + || ((P.$$$ "in" |-- P.xname) >> Target) + + fun config_parser default = (Scan.optional (P.$$$ "(" |-- P.!!! (P.list1 (P.group "option" option_parser)) --| P.$$$ ")") []) + >> (fn opts => fold apply_opt opts default) + + val otherwise = P.$$$ "(" |-- P.$$$ "otherwise" --| P.$$$ ")" + + fun pipe_error t = P.!!! (Scan.fail_with (K (cat_lines ["Equations must be separated by " ^ quote "|", quote t]))) + + val statement_ow = SpecParse.opt_thm_name ":" -- (P.prop -- Scan.optional (otherwise >> K true) false) + --| Scan.ahead ((P.term :-- pipe_error) || Scan.succeed ("","")) + + val statements_ow = P.enum1 "|" statement_ow + + val flags_statements = statements_ow + >> (fn sow => (map (snd o snd) sow, map (apsnd fst) sow)) + + fun basic_apply_flags ((config, fixes), (flags, statements)) = ((config, fixes), statements) +in + fun fundef_parser default_cfg = (config_parser default_cfg -- P.fixes --| P.$$$ "where" -- flags_statements) + +end + + + + + +val default_config = FundefConfig { sequential=false, default="%x. arbitrary", + target=NONE, domintros=false, tailrec=false } diff -r 98736a2fec98 -r a5026e73cfcf src/HOL/Tools/function_package/fundef_datatype.ML --- a/src/HOL/Tools/function_package/fundef_datatype.ML Sat Jun 02 15:26:32 2007 +0200 +++ b/src/HOL/Tools/function_package/fundef_datatype.ML Sat Jun 02 15:28:38 2007 +0200 @@ -14,45 +14,45 @@ val setup : theory -> theory end -structure FundefDatatype : FUNDEF_DATATYPE = +structure FundefDatatype (*: FUNDEF_DATATYPE*) = struct open FundefLib open FundefCommon -fun check_constr_pattern thy err (Bound _) = () - | check_constr_pattern thy err t = - let - val (hd, args) = strip_comb t - in - (((case DatatypePackage.datatype_of_constr thy (fst (dest_Const hd)) of - SOME _ => () - | NONE => err t) - handle TERM ("dest_Const", _) => err t); - map (check_constr_pattern thy err) args; - ()) - end - fun check_pats ctxt geq = let - fun err str = error (cat_lines ["Malformed \"fun\" definition:", - str, + fun err str = error (cat_lines ["Malformed definition:", + str ^ " not allowed in sequential mode.", ProofContext.string_of_term ctxt geq]) val thy = ProofContext.theory_of ctxt - + + fun check_constr_pattern (Bound _) = () + | check_constr_pattern t = + let + val (hd, args) = strip_comb t + in + (((case DatatypePackage.datatype_of_constr thy (fst (dest_Const hd)) of + SOME _ => () + | NONE => err "Non-constructor pattern") + handle TERM ("dest_Const", _) => err "Non-constructor patterns"); + map check_constr_pattern args; + ()) + end + val (fname, qs, gs, args, rhs) = split_def geq - - val _ = if not (null gs) then err "Conditional equations not allowed with \"fun\"" else () - val _ = map (check_constr_pattern thy (fn t => err "Not a constructor pattern")) args - + + val _ = if not (null gs) then err "Conditional equations" else () + val _ = map check_constr_pattern args + (* just count occurrences to check linearity *) val _ = if fold (fold_aterms (fn Bound _ => curry (op +) 1 | _ => I)) args 0 < length qs - then err "Nonlinear pattern" else () + then err "Nonlinear patterns" else () in () end - + fun mk_argvar i T = Free ("_av" ^ (string_of_int i), T) fun mk_patvar i T = Free ("_pv" ^ (string_of_int i), T) @@ -206,27 +206,83 @@ FundefPackage.setup_termination_proof NONE #> Proof.global_terminal_proof (Method.Basic (LexicographicOrder.lexicographic_order []), NONE) +fun mk_catchall fixes arities = + let + fun mk_eqn ((fname, fT), _) = + let + val n = the (Symtab.lookup arities fname) + val (argTs, rT) = chop n (binder_types fT) + |> apsnd (fn Ts => Ts ---> body_type fT) + + val qs = map Free (Name.invent_list [] "a" n ~~ argTs) + in + HOLogic.mk_eq(list_comb (Free (fname, fT), qs), + Const ("HOL.undefined", rT)) + |> HOLogic.mk_Trueprop + |> fold_rev mk_forall qs + end + in + map mk_eqn fixes + end + +fun add_catchall fixes spec = + let + val catchalls = mk_catchall fixes (mk_arities (map split_def (map snd spec))) + in + spec @ map (pair true) catchalls + end + +fun sequential_preproc (config as FundefConfig {sequential, ...}) flags ctxt fixes spec = + let + val enabled = sequential orelse exists I flags + in + if enabled then + let + val flags' = if sequential then map (K true) flags else flags + + val (nas, eqss) = split_list spec + + val eqs = map the_single eqss + + val spliteqs = eqs + |> tap (check_defs ctxt fixes) (* Standard checks *) + |> tap (map (check_pats ctxt)) (* More checks for sequential mode *) + |> curry op ~~ flags' + |> add_catchall fixes (* Completion: still disabled *) + |> FundefSplit.split_some_equations ctxt + + fun restore_spec thms = + nas ~~ Library.take (length nas, Library.unflat spliteqs thms) + in + (flat spliteqs, restore_spec) + end + else + FundefCommon.empty_preproc check_defs config flags ctxt fixes spec + end + val setup = - Method.add_methods [("pat_completeness", Method.no_args pat_completeness, - "Completeness prover for datatype patterns")] + Method.add_methods [("pat_completeness", Method.no_args pat_completeness, + "Completeness prover for datatype patterns")] + #> Context.theory_map (FundefCommon.set_preproc sequential_preproc) +val fun_config = FundefConfig { sequential=true, default="%x. arbitrary", + target=NONE, domintros=false, tailrec=false } local structure P = OuterParse and K = OuterKeyword in -fun fun_cmd config fixes statements lthy = +fun fun_cmd config fixes statements flags lthy = lthy - |> FundefPackage.add_fundef fixes statements config + |> FundefPackage.add_fundef fixes statements config flags |> by_pat_completeness_simp |> termination_by_lexicographic_order - val funP = OuterSyntax.command "fun" "define general recursive functions (short version)" K.thy_decl - (fundef_parser FundefCommon.fun_config - >> (fn ((config, fixes), statements) => - (Toplevel.local_theory (target_of config) (fun_cmd config fixes statements)))); + (fundef_parser fun_config + >> (fn ((config, fixes), (flags, statements)) => + (Toplevel.local_theory (target_of config) (fun_cmd config fixes statements flags)))); val _ = OuterSyntax.add_parsers [funP]; end diff -r 98736a2fec98 -r a5026e73cfcf src/HOL/Tools/function_package/fundef_lib.ML --- a/src/HOL/Tools/function_package/fundef_lib.ML Sat Jun 02 15:26:32 2007 +0200 +++ b/src/HOL/Tools/function_package/fundef_lib.ML Sat Jun 02 15:28:38 2007 +0200 @@ -10,12 +10,6 @@ structure FundefLib = struct -(* ==> library/string *) -fun plural sg pl [x] = sg - | plural sg pl _ = pl - - - fun map_option f NONE = NONE | map_option f (SOME x) = SOME (f x); @@ -25,11 +19,6 @@ fun fold_map_option f NONE y = (NONE, y) | fold_map_option f (SOME x) y = apfst SOME (f x y); - - - - - (* ??? *) fun eq_str (s : string, t) = (s = t) (* monomorphic equality on strings *) diff -r 98736a2fec98 -r a5026e73cfcf src/HOL/Tools/function_package/fundef_package.ML --- a/src/HOL/Tools/function_package/fundef_package.ML Sat Jun 02 15:26:32 2007 +0200 +++ b/src/HOL/Tools/function_package/fundef_package.ML Sat Jun 02 15:28:38 2007 +0200 @@ -10,14 +10,16 @@ signature FUNDEF_PACKAGE = sig val add_fundef : (string * string option * mixfix) list - -> ((bstring * Attrib.src list) * (string * bool)) list + -> ((bstring * Attrib.src list) * string) list -> FundefCommon.fundef_config + -> bool list -> local_theory -> Proof.state val add_fundef_i: (string * typ option * mixfix) list - -> ((bstring * Attrib.src list) * (term * bool)) list + -> ((bstring * Attrib.src list) * term) list -> FundefCommon.fundef_config + -> bool list -> local_theory -> Proof.state @@ -32,7 +34,7 @@ end -structure FundefPackage (*: FUNDEF_PACKAGE*) = +structure FundefPackage : FUNDEF_PACKAGE = struct open FundefLib @@ -42,80 +44,12 @@ fun mk_defname fixes = fixes |> map (fst o fst) |> space_implode "_" - -(* Check for all sorts of errors in the input *) -fun check_def ctxt fixes eqs = - let - val fnames = map (fst o fst) fixes - - fun check geq = - let - fun input_error msg = cat_lines [msg, ProofContext.string_of_term ctxt geq] - - val fqgar as (fname, qs, gs, args, rhs) = split_def geq - - val _ = fname mem fnames - orelse error (input_error ("Head symbol of left hand side must be " ^ plural "" "one out of " fnames - ^ commas_quote fnames)) - - 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 _ = null rvs orelse error (input_error ("Variable" ^ plural " " "s " rvs ^ commas_quote rvs - ^ " occur" ^ plural "s" "" rvs ^ " on right hand side only:")) - - val _ = forall (forall_aterms (fn Free (n, _) => not (n mem fnames) | _ => true)) gs orelse - error (input_error "Recursive Calls not allowed in premises") - in - fqgar - end - in - (mk_arities (map check eqs); ()) - handle ArgumentCount fname => - error ("Function " ^ quote fname ^ " has different numbers of arguments in different equations") - end - - -fun mk_catchall fixes arities = - let - fun mk_eqn ((fname, fT), _) = - let - val n = the (Symtab.lookup arities fname) - val (argTs, rT) = chop n (binder_types fT) - |> apsnd (fn Ts => Ts ---> body_type fT) - - val qs = map Free (Name.invent_list [] "a" n ~~ argTs) - in - HOLogic.mk_eq(list_comb (Free (fname, fT), qs), - Const ("HOL.undefined", rT)) - |> HOLogic.mk_Trueprop - |> fold_rev mk_forall qs - end - in - map mk_eqn fixes - end - -fun add_catchall fixes spec = - let - val catchalls = mk_catchall fixes (mk_arities (map split_def (map (snd o snd) spec))) - in - spec @ map (pair ("",[]) o pair true) catchalls - end - -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 - -fun restore_spec_structure reps spec = - (burrow_snd o burrow o K) reps spec - -fun add_simps fixes spec sort label moreatts simps lthy = +fun add_simps fixes post sort label moreatts simps lthy = let val fnames = map (fst o fst) fixes val (saved_spec_simps, lthy) = - fold_map note_theorem (restore_spec_structure simps spec) lthy + fold_map note_theorem (post simps) lthy val saved_simps = flat (map snd saved_spec_simps) val simps_by_f = sort saved_simps @@ -129,13 +63,13 @@ fold2 add_for_f fnames simps_by_f lthy) end -fun fundef_afterqed config fixes spec defname cont sort_cont [[proof]] lthy = +fun fundef_afterqed config fixes post defname cont sort_cont [[proof]] lthy = let val FundefResult {fs, R, psimps, trsimps, subset_pinducts, simple_pinducts, termination, domintros, cases, ...} = cont (Goal.close_result proof) val qualify = NameSpace.qualified defname - val addsmps = add_simps fixes spec sort_cont + val addsmps = add_simps fixes post sort_cont val (((psimps', pinducts'), (_, [termination'])), lthy) = lthy @@ -157,52 +91,36 @@ end (* FIXME: Add cases for induct and cases thm *) - -fun prep_with_flags prep fixspec eqnss_flags global_flag lthy = +fun prepare_spec prep fixspec eqnss lthy = (* FIXME: obsolete when "read_specification" etc. is there *) let - val flags = map (fn x => global_flag orelse (snd (snd x))) eqnss_flags - val eqns = map (apsnd (single o fst)) eqnss_flags - - val ((fixes, _), ctxt') = prep fixspec [] lthy - - fun prep_eqn e = the_single (snd (fst (prep [] [e] ctxt'))) - |> apsnd the_single + val eqns = map (apsnd single) eqnss - val raw_spec = map prep_eqn eqns - |> map (apsnd (fn t => fold_rev (mk_forall o Free) (frees_in_term ctxt' t) t)) (* Add quantifiers *) - - val _ = check_def ctxt' fixes (map snd raw_spec) + val ((fixes, _), ctxt') = prep fixspec [] lthy + fun prep_eqn e = the_single (snd (fst (prep [] [e] ctxt'))) - val spec = raw_spec - |> burrow_snd (fn ts => flags ~~ ts) - (*|> (if global_flag then add_catchall fixes else I) *) (* Completion: still disabled *) - |> burrow_snd (FundefSplit.split_some_equations ctxt') - + val spec = map prep_eqn eqns + |> map (apsnd (map (fn t => fold_rev (mk_forall o Free) (frees_in_term ctxt' t) t))) (* Add quantifiers *) in ((fixes, spec), ctxt') end -fun gen_add_fundef prep_spec fixspec eqnss_flags config lthy = +fun gen_add_fundef prep fixspec eqnss config flags lthy = let - val FundefConfig {sequential, ...} = config - - val ((fixes, spec), ctxt') = prep_with_flags prep_spec fixspec eqnss_flags sequential lthy + val ((fixes, spec), ctxt') = prepare_spec prep fixspec eqnss lthy + val (eqs, post) = FundefCommon.get_preproc lthy config flags ctxt' fixes spec val defname = mk_defname fixes - val t_eqns = spec |> map snd |> flat (* flatten external structure *) + val ((goalstate, cont, sort_cont), lthy) = + FundefMutual.prepare_fundef_mutual config defname fixes eqs lthy - val ((goalstate, cont, sort_cont), lthy) = - FundefMutual.prepare_fundef_mutual config defname fixes t_eqns lthy - - val afterqed = fundef_afterqed config fixes spec defname cont sort_cont + val afterqed = fundef_afterqed config fixes post defname cont sort_cont in lthy |> Proof.theorem_i NONE afterqed [[(Logic.unprotect (concl_of goalstate), [])]] |> Proof.refine (Method.primitive_text (fn _ => goalstate)) |> Seq.hd end - fun total_termination_afterqed data [[totality]] lthy = let val FundefCtxData { add_simps, psimps, pinducts, defname, ... } = data @@ -214,7 +132,6 @@ val tsimps = map remove_domain_condition psimps val tinduct = map remove_domain_condition pinducts - (* FIXME: How to generate code from (possibly) local contexts*) val has_guards = exists ((fn (Const ("Trueprop", _) $ _) => false | _ => true) o prop_of) tsimps val allatts = if has_guards then [] else [Attrib.internal (K (RecfunCodegen.add NONE))] @@ -293,8 +210,8 @@ val functionP = OuterSyntax.command "function" "define general recursive functions" K.thy_goal (fundef_parser default_config - >> (fn ((config, fixes), statements) => - Toplevel.local_theory_to_proof (target_of config) (add_fundef fixes statements config) + >> (fn ((config, fixes), (flags, statements)) => + Toplevel.local_theory_to_proof (target_of config) (add_fundef fixes statements config flags) #> Toplevel.print)); val terminationP = diff -r 98736a2fec98 -r a5026e73cfcf src/HOL/Tools/function_package/mutual.ML --- a/src/HOL/Tools/function_package/mutual.ML Sat Jun 02 15:26:32 2007 +0200 +++ b/src/HOL/Tools/function_package/mutual.ML Sat Jun 02 15:28:38 2007 +0200 @@ -303,7 +303,7 @@ fun sort_by_function (Mutual {fqgars, ...}) names xs = fold_rev (store_grouped (eq_str o apfst fst)) (* fill *) - (map name_of_fqgar fqgars ~~ xs) (* the name-thm pairs *) + (map name_of_fqgar (Library.take (length xs, fqgars)) ~~ xs) (* the name-thm pairs *) (map (rpair []) names) (* in the empty buckets labeled with names *) |> map (snd #> map snd) (* and remove the labels afterwards *)