added profiling code, improved handling of proof terms, generation of domain
authorkrauss
Wed Nov 08 22:24:54 2006 +0100 (2006-11-08)
changeset 21255617fdb08abe9
parent 21254 d53f76357f41
child 21256 47195501ecf7
added profiling code, improved handling of proof terms, generation of domain
introduction rules becomes optional (global reference FundefCommon.domintros)
src/HOL/Tools/function_package/fundef_common.ML
src/HOL/Tools/function_package/fundef_package.ML
src/HOL/Tools/function_package/fundef_prep.ML
src/HOL/Tools/function_package/fundef_proof.ML
src/HOL/Tools/function_package/mutual.ML
src/HOL/Tools/function_package/termination.ML
     1.1 --- a/src/HOL/Tools/function_package/fundef_common.ML	Wed Nov 08 21:45:15 2006 +0100
     1.2 +++ b/src/HOL/Tools/function_package/fundef_common.ML	Wed Nov 08 22:24:54 2006 +0100
     1.3 @@ -12,6 +12,11 @@
     1.4  (* Theory Dependencies *)
     1.5  val acc_const_name = "FunDef.accP"
     1.6  
     1.7 +val domintros = ref true;
     1.8 +val profile = ref false;
     1.9 +
    1.10 +fun PROFILE msg = if !profile then timeap_msg msg else I
    1.11 +
    1.12  fun mk_acc domT R =
    1.13      Const (acc_const_name, (fastype_of R) --> domT --> HOLogic.boolT) $ R 
    1.14  
    1.15 @@ -175,14 +180,26 @@
    1.16        domintros : thm list
    1.17       }
    1.18  
    1.19 +datatype fundef_context_data =
    1.20 +  FundefCtxData of
    1.21 +     {
    1.22 +      fixes : ((string * typ) * mixfix) list,
    1.23 +      spec : ((string * Attrib.src list) * term list) list list,
    1.24 +      mutual: mutual_info,
    1.25  
    1.26 -type fundef_spec = ((string * typ) * mixfix) list *((string * Attrib.src list) * term list) list list
    1.27 -type result_with_names = fundef_mresult * mutual_info * fundef_spec
    1.28 +      f : term,
    1.29 +      R : term,
    1.30 +      
    1.31 +      psimps: thm list,
    1.32 +      pinducts: thm list,
    1.33 +      termination: thm
    1.34 +     }
    1.35 +
    1.36  
    1.37  structure FundefData = GenericDataFun
    1.38  (struct
    1.39    val name = "HOL/function_def/data";
    1.40 -  type T = string * result_with_names Symtab.table
    1.41 +  type T = string * fundef_context_data Symtab.table
    1.42  
    1.43    val empty = ("", Symtab.empty);
    1.44    val copy = I;
    1.45 @@ -206,10 +223,11 @@
    1.46  
    1.47  
    1.48  fun add_fundef_data name fundef_data =
    1.49 -    FundefData.map (fn (_,tab) => (name, Symtab.update_new (name, fundef_data) tab))
    1.50 +    FundefData.map (fn (last,tab) => (name, Symtab.update_new (name, fundef_data) tab))
    1.51  
    1.52  fun get_fundef_data name thy = Symtab.lookup (snd (FundefData.get thy)) name
    1.53  
    1.54 +fun set_last_fundef name = FundefData.map (apfst (K name))
    1.55  fun get_last_fundef thy = fst (FundefData.get thy)
    1.56  
    1.57  val map_fundef_congs = FundefCongs.map 
     2.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Wed Nov 08 21:45:15 2006 +0100
     2.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Wed Nov 08 22:24:54 2006 +0100
     2.3 @@ -50,31 +50,43 @@
     2.4  fun add_simps label moreatts mutual_info fixes psimps spec lthy =
     2.5      let
     2.6        val fnames = map (fst o fst) fixes
     2.7 -      val psimps_by_f = FundefMutual.sort_by_function mutual_info fnames psimps
     2.8 +
     2.9 +      val (saved_spec_psimps, lthy) = fold_map (fold_map LocalTheory.note) (restore_spec_structure psimps spec) lthy
    2.10 +      val saved_psimps = flat (map snd (flat saved_spec_psimps))
    2.11 +
    2.12 +      val psimps_by_f = FundefMutual.sort_by_function mutual_info fnames saved_psimps
    2.13  
    2.14        fun add_for_f fname psimps =
    2.15            LocalTheory.note ((NameSpace.append fname label, Attrib.internal Simplifier.simp_add :: moreatts), psimps) #> snd
    2.16      in
    2.17 -      lthy
    2.18 -        |> fold_map (fold_map LocalTheory.note) (restore_spec_structure psimps spec) |> snd
    2.19 -        |> fold2 add_for_f fnames psimps_by_f
    2.20 +      (saved_psimps,
    2.21 +       fold2 add_for_f fnames psimps_by_f lthy)
    2.22      end
    2.23  
    2.24  
    2.25  fun fundef_afterqed fixes spec mutual_info defname data [[result]] lthy =
    2.26      let
    2.27 -        val fundef_data = FundefMutual.mk_partial_rules_mutual lthy mutual_info data result
    2.28 -        val FundefMResult {psimps, subset_pinducts, simple_pinducts, termination, domintros, cases, ...} = fundef_data
    2.29 -        val qualify = NameSpace.append defname;
    2.30 +      val Prep {f, R, ...} = data
    2.31 +      val fundef_data = FundefMutual.mk_partial_rules_mutual lthy mutual_info data result
    2.32 +      val FundefMResult {psimps, subset_pinducts, simple_pinducts, termination, domintros, cases, ...} = fundef_data
    2.33 +      val qualify = NameSpace.append defname
    2.34 +          
    2.35 +      val (((psimps', pinducts'), (_, [termination'])), lthy) = 
    2.36 +          lthy
    2.37 +            |> PROFILE "adding_psimps" (add_simps "psimps" [] mutual_info fixes psimps spec)
    2.38 +            ||>> PROFILE "adding pinduct" (LocalTheory.note ((qualify "pinduct", [Attrib.internal (InductAttrib.induct_set "")]), simple_pinducts))
    2.39 +            ||>> PROFILE "adding termination" (LocalTheory.note ((qualify "termination", []), [termination]))
    2.40 +            ||> (snd o PROFILE "adding cases" (LocalTheory.note ((qualify "cases", []), [cases])))
    2.41 +            ||> (snd o PROFILE "adding domintros" (LocalTheory.note ((qualify "domintros", []), domintros)))
    2.42 +
    2.43 +      val cdata = FundefCtxData { fixes=fixes, spec=spec, mutual=mutual_info, psimps=psimps',
    2.44 +                                  pinducts=snd pinducts', termination=termination', f=f, R=R }
    2.45 +
    2.46 +      
    2.47      in
    2.48        lthy
    2.49 -        |> add_simps "psimps" [] mutual_info fixes psimps spec
    2.50 -        |> LocalTheory.note ((qualify "domintros", []), domintros) |> snd
    2.51 -        |> LocalTheory.note ((qualify "termination", []), [termination]) |> snd
    2.52 -        |> LocalTheory.note ((qualify "cases", []), [cases]) |> snd
    2.53 -        |> LocalTheory.note ((qualify "pinduct", [Attrib.internal (InductAttrib.induct_set "")]), simple_pinducts) |> snd
    2.54 -        |> LocalTheory.declaration (add_fundef_data defname (fundef_data, mutual_info, (fixes,spec))) (* save in target *)
    2.55 -        |> Context.proof_map (add_fundef_data defname (fundef_data, mutual_info, (fixes,spec))) (* also save in local context *)
    2.56 +        |> LocalTheory.declaration (add_fundef_data defname cdata) (* save in target *)
    2.57 +        |> Context.proof_map (add_fundef_data defname cdata) (* also save in local context *)
    2.58      end (* FIXME: Add cases for induct and cases thm *)
    2.59  
    2.60  
    2.61 @@ -117,12 +129,14 @@
    2.62  
    2.63  fun total_termination_afterqed defname data [[totality]] lthy =
    2.64      let
    2.65 -        val (FundefMResult {psimps, simple_pinducts, ... }, mutual_info, (fixes, stmts)) = data
    2.66 +      val FundefCtxData { fixes, spec, mutual, psimps, pinducts, ... } = data
    2.67 +
    2.68 +      val totality = PROFILE "closing" Drule.close_derivation totality
    2.69  
    2.70 -        val remove_domain_condition = full_simplify (HOL_basic_ss addsimps [totality, True_implies_equals])
    2.71 +      val remove_domain_condition = full_simplify (HOL_basic_ss addsimps [totality, True_implies_equals])
    2.72  
    2.73 -        val tsimps = map remove_domain_condition psimps
    2.74 -        val tinduct = map remove_domain_condition simple_pinducts
    2.75 +      val tsimps = PROFILE "making tsimps" (map remove_domain_condition) psimps
    2.76 +      val tinduct = PROFILE "making tinduct" (map remove_domain_condition) pinducts
    2.77  
    2.78          (* FIXME: How to generate code from (possibly) local contexts
    2.79          val has_guards = exists ((fn (Const ("Trueprop", _) $ _) => false | _ => true) o prop_of) tsimps
    2.80 @@ -131,8 +145,8 @@
    2.81          val qualify = NameSpace.append defname;
    2.82      in
    2.83          lthy
    2.84 -          |> add_simps "simps" [] mutual_info fixes tsimps stmts
    2.85 -          |> LocalTheory.note ((qualify "induct", []), tinduct) |> snd
    2.86 +          |> PROFILE "adding tsimps" (add_simps "simps" [] mutual fixes tsimps spec) |> snd
    2.87 +          |> PROFILE "adding tinduct" (LocalTheory.note ((qualify "induct", []), tinduct)) |> snd
    2.88      end
    2.89  
    2.90  
    2.91 @@ -142,8 +156,8 @@
    2.92          val data = the (get_fundef_data name (Context.Proof lthy))
    2.93                     handle Option.Option => raise ERROR ("No such function definition: " ^ name)
    2.94  
    2.95 -        val (res as FundefMResult {termination, ...}, _, _) = data
    2.96 -        val goal = FundefTermination.mk_total_termination_goal data
    2.97 +        val FundefCtxData {termination, f, R, ...} = data
    2.98 +        val goal = FundefTermination.mk_total_termination_goal f R
    2.99      in
   2.100        lthy
   2.101          |> ProofContext.note_thmss_i [(("termination",
     3.1 --- a/src/HOL/Tools/function_package/fundef_prep.ML	Wed Nov 08 21:45:15 2006 +0100
     3.2 +++ b/src/HOL/Tools/function_package/fundef_prep.ML	Wed Nov 08 22:24:54 2006 +0100
     3.3 @@ -477,6 +477,8 @@
     3.4        val fvar = Free (fname, fT)
     3.5        val domT = domain_type fT
     3.6        val ranT = range_type fT
     3.7 +
     3.8 +                 
     3.9                              
    3.10        val [default] = fst (Variable.importT_terms (fst (ProofContext.read_termTs lthy (K false) (K NONE) (K NONE) [] [(default_str, fT)])) lthy) (* FIXME *)
    3.11  
    3.12 @@ -485,7 +487,7 @@
    3.13  
    3.14        val Globals { x, h, ... } = globals
    3.15  
    3.16 -      val clauses = map (mk_clause_context x ctxt') abstract_qglrs 
    3.17 +      val clauses = PROFILE "mk_clause_context" (map (mk_clause_context x ctxt')) abstract_qglrs 
    3.18  
    3.19        val n = length abstract_qglrs
    3.20  
    3.21 @@ -494,34 +496,34 @@
    3.22        fun build_tree (ClauseContext { ctxt, rhs, ...}) = 
    3.23              FundefCtxTree.mk_tree congs_deps (fname, fT) h ctxt rhs
    3.24  
    3.25 -      val trees = map build_tree clauses
    3.26 -      val RCss = map find_calls trees
    3.27 +      val trees = PROFILE "making trees" (map build_tree) clauses
    3.28 +      val RCss = PROFILE "finding calls" (map find_calls) trees
    3.29  
    3.30 -      val ((G, GIntro_thms, G_elim), lthy) = define_graph (defname ^ "_graph") fvar domT ranT clauses RCss lthy
    3.31 -      val ((f, f_defthm), lthy) = define_function (defname ^ "_sum_def") (fname, mixfix) domT ranT G default lthy
    3.32 +      val ((G, GIntro_thms, G_elim), lthy) = PROFILE "def_graph" (define_graph (defname ^ "_graph") fvar domT ranT clauses RCss) lthy
    3.33 +      val ((f, f_defthm), lthy) = PROFILE "def_fun" (define_function (defname ^ "_sum_def") (fname, mixfix) domT ranT G default) lthy
    3.34  
    3.35 -      val RCss = map (map (inst_RC (ProofContext.theory_of lthy) fvar f)) RCss
    3.36 -      val trees = map (FundefCtxTree.inst_tree (ProofContext.theory_of lthy) fvar f) trees
    3.37 +      val RCss = PROFILE "inst_RCs" (map (map (inst_RC (ProofContext.theory_of lthy) fvar f))) RCss
    3.38 +      val trees = PROFILE "inst_trees" (map (FundefCtxTree.inst_tree (ProofContext.theory_of lthy) fvar f)) trees
    3.39  
    3.40        val ((R, RIntro_thmss, R_elim), lthy) = 
    3.41 -          define_recursion_relation (defname ^ "_rel") domT ranT fvar f abstract_qglrs clauses RCss lthy
    3.42 +          PROFILE "def_rel" (define_recursion_relation (defname ^ "_rel") domT ranT fvar f abstract_qglrs clauses RCss) lthy
    3.43  
    3.44        val dom_abbrev = Logic.mk_equals (Free (defname ^ "_dom", domT --> boolT), mk_acc domT R)
    3.45 -      val lthy = Specification.abbreviation_i ("", false) [(NONE, dom_abbrev)] lthy
    3.46 +      val lthy = PROFILE "abbrev" (Specification.abbreviation_i ("", false) [(NONE, dom_abbrev)]) lthy
    3.47  
    3.48        val newthy = ProofContext.theory_of lthy
    3.49        val clauses = map (transfer_clause_ctx newthy) clauses
    3.50  
    3.51        val cert = cterm_of (ProofContext.theory_of lthy)
    3.52  
    3.53 -      val xclauses = map7 (mk_clause_info globals G f) (1 upto n) clauses abstract_qglrs trees RCss GIntro_thms RIntro_thmss
    3.54 +      val xclauses = PROFILE "xclauses" (map7 (mk_clause_info globals G f) (1 upto n) clauses abstract_qglrs trees RCss GIntro_thms) RIntro_thmss
    3.55  
    3.56 -      val complete = mk_completeness globals clauses abstract_qglrs |> cert |> assume
    3.57 -      val compat = mk_compat_proof_obligations domT ranT fvar f abstract_qglrs |> map (cert #> assume)
    3.58 +      val complete = PROFILE "mk_compl" (mk_completeness globals clauses) abstract_qglrs |> cert |> assume
    3.59 +      val compat = PROFILE "mk_compat" (mk_compat_proof_obligations domT ranT fvar f) abstract_qglrs |> map (cert #> assume)
    3.60  
    3.61        val compat_store = store_compat_thms n compat
    3.62  
    3.63 -      val (goal, goalI, ex1_iff, values) = prove_stuff newthy congs globals G f R xclauses complete compat compat_store G_elim f_defthm
    3.64 +      val (goal, goalI, ex1_iff, values) = PROFILE "prove_stuff" (prove_stuff newthy congs globals G f R xclauses complete compat compat_store G_elim) f_defthm
    3.65      in
    3.66          (Prep {globals = globals, f = f, G = G, R = R, goal = goal, goalI = goalI, values = values, clauses = xclauses, ex1_iff = ex1_iff, R_cases = R_elim}, f,
    3.67           lthy)
     4.1 --- a/src/HOL/Tools/function_package/fundef_proof.ML	Wed Nov 08 21:45:15 2006 +0100
     4.2 +++ b/src/HOL/Tools/function_package/fundef_proof.ML	Wed Nov 08 22:24:54 2006 +0100
     4.3 @@ -43,11 +43,11 @@
     4.4  
     4.5  fun mk_psimp thy globals R f_iff graph_is_function clause valthm =
     4.6      let
     4.7 -  val Globals {domT, z, ...} = globals
     4.8 -
     4.9 -  val ClauseInfo {qglr = (oqs, _, _, _), cdata = ClauseContext {qs, cqs, gs, lhs, rhs, ags, ...}, ...} = clause
    4.10 -  val lhs_acc = cterm_of thy (Trueprop (mk_acc domT R $ lhs)) (* "acc R lhs" *)
    4.11 -  val z_smaller = cterm_of thy (Trueprop (R $ z $ lhs)) (* "R z lhs" *)
    4.12 +      val Globals {domT, z, ...} = globals
    4.13 +                                   
    4.14 +      val ClauseInfo {qglr = (oqs, _, _, _), cdata = ClauseContext {qs, cqs, gs, lhs, rhs, ags, ...}, ...} = clause
    4.15 +      val lhs_acc = cterm_of thy (Trueprop (mk_acc domT R $ lhs)) (* "acc R lhs" *)
    4.16 +      val z_smaller = cterm_of thy (Trueprop (R $ z $ lhs)) (* "R z lhs" *)
    4.17      in
    4.18        ((assume z_smaller) RS ((assume lhs_acc) RS acc_downward))
    4.19          |> (fn it => it COMP graph_is_function)
    4.20 @@ -64,29 +64,29 @@
    4.21  
    4.22  fun mk_partial_induct_rule thy globals R complete_thm clauses =
    4.23      let
    4.24 -  val Globals {domT, x, z, a, P, D, ...} = globals
    4.25 -        val acc_R = mk_acc domT R
    4.26 -
    4.27 -  val x_D = assume (cterm_of thy (Trueprop (D $ x)))
    4.28 -  val a_D = cterm_of thy (Trueprop (D $ a))
    4.29 -
    4.30 -  val D_subset = cterm_of thy (mk_forall x (implies $ Trueprop (D $ x) $ Trueprop (acc_R $ x)))
    4.31 -
    4.32 -  val D_dcl = (* "!!x z. [| x: D; (z,x):R |] ==> z:D" *)
    4.33 -      mk_forall x
    4.34 -          (mk_forall z (Logic.mk_implies (Trueprop (D $ x),
    4.35 -                  Logic.mk_implies (Trueprop (R $ z $ x),
    4.36 -                  Trueprop (D $ z)))))
    4.37 -          |> cterm_of thy
    4.38 -
    4.39 -
    4.40 +      val Globals {domT, x, z, a, P, D, ...} = globals
    4.41 +      val acc_R = mk_acc domT R
    4.42 +                  
    4.43 +      val x_D = assume (cterm_of thy (Trueprop (D $ x)))
    4.44 +      val a_D = cterm_of thy (Trueprop (D $ a))
    4.45 +                
    4.46 +      val D_subset = cterm_of thy (mk_forall x (implies $ Trueprop (D $ x) $ Trueprop (acc_R $ x)))
    4.47 +                     
    4.48 +      val D_dcl = (* "!!x z. [| x: D; (z,x):R |] ==> z:D" *)
    4.49 +                    mk_forall x
    4.50 +                    (mk_forall z (Logic.mk_implies (Trueprop (D $ x),
    4.51 +                                                    Logic.mk_implies (Trueprop (R $ z $ x),
    4.52 +                                                                      Trueprop (D $ z)))))
    4.53 +                    |> cterm_of thy
    4.54 +                    
    4.55 +                    
    4.56    (* Inductive Hypothesis: !!z. (z,x):R ==> P z *)
    4.57 -  val ihyp = all domT $ Abs ("z", domT, 
    4.58 -           implies $ Trueprop (R $ Bound 0 $ x)
    4.59 +      val ihyp = all domT $ Abs ("z", domT, 
    4.60 +               implies $ Trueprop (R $ Bound 0 $ x)
    4.61               $ Trueprop (P $ Bound 0))
    4.62             |> cterm_of thy
    4.63  
    4.64 -  val aihyp = assume ihyp
    4.65 +      val aihyp = assume ihyp
    4.66  
    4.67    fun prove_case clause =
    4.68        let
    4.69 @@ -188,6 +188,9 @@
    4.70      end
    4.71  
    4.72  
    4.73 +fun maybe_mk_domain_intro thy =
    4.74 +    if !FundefCommon.domintros then mk_domain_intro thy
    4.75 +    else K (K (K (K refl)))
    4.76  
    4.77  
    4.78  fun mk_nest_term_case thy globals R' ihyp clause =
    4.79 @@ -296,34 +299,22 @@
    4.80      let
    4.81        val Prep {globals, G, f, R, clauses, values, R_cases, ex1_iff, ...} = data
    4.82                                                                              
    4.83 -      val _ = Output.debug "Closing Derivation"
    4.84 -              
    4.85 -      val provedgoal = Drule.close_derivation provedgoal
    4.86 +      val provedgoal = PROFILE "Closing Derivation" Drule.close_derivation provedgoal
    4.87                         
    4.88 -      val _ = Output.debug "Getting function theorem"
    4.89 -              
    4.90 -      val graph_is_function = (provedgoal COMP conjunctionD1)
    4.91 -                                |> forall_elim_vars 0
    4.92 +      val graph_is_function = PROFILE "Getting function theorem" (fn x => (x COMP conjunctionD1) |> forall_elim_vars 0) provedgoal
    4.93                                
    4.94 -      val _ = Output.debug "Getting cases"
    4.95 -              
    4.96 -      val complete_thm = provedgoal COMP conjunctionD2
    4.97 -                         
    4.98 -      val _ = Output.debug "Making f_iff"
    4.99 -              
   4.100 -      val f_iff = (graph_is_function RS ex1_iff) 
   4.101 +      val complete_thm = PROFILE "Getting cases" (curry op COMP provedgoal) conjunctionD2
   4.102 +
   4.103 +      val f_iff = PROFILE "Making f_iff" (curry op RS graph_is_function) ex1_iff
   4.104                    
   4.105 -      val _ = Output.debug "Proving simplification rules"
   4.106 -      val psimps  = map2 (mk_psimp thy globals R f_iff graph_is_function) clauses values
   4.107 +      val psimps = PROFILE "Proving simplification rules" (map2 (mk_psimp thy globals R f_iff graph_is_function)) clauses values
   4.108                      
   4.109 -      val _ = Output.debug "Proving partial induction rule"
   4.110 -      val (subset_pinduct, simple_pinduct) = mk_partial_induct_rule thy globals R complete_thm clauses
   4.111 +      val (subset_pinduct, simple_pinduct) = PROFILE "Proving partial induction rule" 
   4.112 +                                             (mk_partial_induct_rule thy globals R complete_thm) clauses
   4.113                                               
   4.114 -      val _ = Output.debug "Proving nested termination rule"
   4.115 -      val total_intro = mk_nest_term_rule thy globals R R_cases clauses
   4.116 +      val total_intro = PROFILE "Proving nested termination rule" (mk_nest_term_rule thy globals R R_cases) clauses
   4.117                          
   4.118 -      val _ = Output.debug "Proving domain introduction rules"
   4.119 -      val dom_intros = map (mk_domain_intro thy globals R R_cases) clauses
   4.120 +      val dom_intros = PROFILE "Proving domain introduction rules" (map (maybe_mk_domain_intro thy globals R R_cases)) clauses
   4.121      in 
   4.122        FundefResult {f=f, G=G, R=R, completeness=complete_thm, 
   4.123                      psimps=psimps, subset_pinduct=subset_pinduct, simple_pinduct=simple_pinduct, total_intro=total_intro,
     5.1 --- a/src/HOL/Tools/function_package/mutual.ML	Wed Nov 08 21:45:15 2006 +0100
     5.2 +++ b/src/HOL/Tools/function_package/mutual.ML	Wed Nov 08 22:24:54 2006 +0100
     5.3 @@ -337,10 +337,9 @@
     5.4        fun mk_mpsimp fqgar sum_psimp =
     5.5            in_context lthy fqgar (recover_mutual_psimp thy RST streeR all_f_defs parts) sum_psimp
     5.6            
     5.7 -      val mpsimps = map2 mk_mpsimp fqgars psimps
     5.8 -                    
     5.9 -      val minducts = mutual_induct_rules thy simple_pinduct all_f_defs m
    5.10 -      val termination = full_simplify (HOL_basic_ss addsimps all_f_defs) total_intro
    5.11 +      val mpsimps = PROFILE "making mpsimps" (map2 mk_mpsimp fqgars) psimps
    5.12 +      val minducts = PROFILE "making mpinduct" (mutual_induct_rules thy simple_pinduct all_f_defs) m
    5.13 +      val termination = PROFILE "making mtermination" (full_simplify (HOL_basic_ss addsimps all_f_defs)) total_intro
    5.14      in
    5.15        FundefMResult { f=expand_term f, G=expand_term G, R=expand_term R,
    5.16                        psimps=map expand mpsimps, subset_pinducts=[expand subset_pinduct], simple_pinducts=map expand minducts,
     6.1 --- a/src/HOL/Tools/function_package/termination.ML	Wed Nov 08 21:45:15 2006 +0100
     6.2 +++ b/src/HOL/Tools/function_package/termination.ML	Wed Nov 08 22:24:54 2006 +0100
     6.3 @@ -9,8 +9,8 @@
     6.4  
     6.5  signature FUNDEF_TERMINATION =
     6.6  sig
     6.7 -  val mk_total_termination_goal : FundefCommon.result_with_names -> term
     6.8 -  val mk_partial_termination_goal : theory -> FundefCommon.result_with_names -> string -> term * term
     6.9 +  val mk_total_termination_goal : term -> term -> term
    6.10 +(*  val mk_partial_termination_goal : theory -> FundefCommon.result_with_names -> string -> term * term*)
    6.11  end
    6.12  
    6.13  structure FundefTermination : FUNDEF_TERMINATION =
    6.14 @@ -21,7 +21,7 @@
    6.15  open FundefCommon
    6.16  open FundefAbbrev
    6.17       
    6.18 -fun mk_total_termination_goal (FundefMResult {R, f, ... }, _, _) =
    6.19 +fun mk_total_termination_goal f R =
    6.20      let
    6.21        val domT = domain_type (fastype_of f)
    6.22        val x = Free ("x", domT)
    6.23 @@ -29,6 +29,7 @@
    6.24        mk_forall x (Trueprop (mk_acc domT R $ x))
    6.25      end
    6.26      
    6.27 +(*
    6.28  fun mk_partial_termination_goal thy (FundefMResult {R, f, ... }, _, _) dom =
    6.29      let
    6.30        val domT = domain_type (fastype_of f)
    6.31 @@ -55,7 +56,7 @@
    6.32      in
    6.33        (subs, dcl)
    6.34      end
    6.35 -
    6.36 +*)
    6.37  end
    6.38  
    6.39