function-package: Changed record usage to make sml/nj happy...
authorkrauss
Sun May 07 00:00:13 2006 +0200 (2006-05-07)
changeset 19583c5fa77b03442
parent 19582 a669c98b9c24
child 19584 606d6a73e6d9
function-package: Changed record usage to make sml/nj happy...
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/termination.ML
src/HOL/ex/Fundefs.thy
     1.1 --- a/src/HOL/Tools/function_package/fundef_common.ML	Fri May 05 22:11:19 2006 +0200
     1.2 +++ b/src/HOL/Tools/function_package/fundef_common.ML	Sun May 07 00:00:13 2006 +0200
     1.3 @@ -29,8 +29,8 @@
     1.4  
     1.5  (* A record containing all the relevant symbols and types needed during the proof.
     1.6     This is set up at the beginning and does not change. *)
     1.7 -type naming_context =
     1.8 -     { f: term, fvarname: string, fvar: term, domT: typ, ranT: typ,
     1.9 +datatype naming_context =
    1.10 +   Names of { f: term, fvarname: string, fvar: term, domT: typ, ranT: typ,
    1.11         G: term, R: term, acc_R: term, h: term, y: term, x: term, z: term, a:term, P: term, 
    1.12         D: term, Pbool:term,
    1.13         glrs: (term list * term list * term * term) list,
    1.14 @@ -41,10 +41,11 @@
    1.15       }
    1.16  
    1.17  
    1.18 -type rec_call_info = 
    1.19 -     {RI: thm, RIvs: (string * typ) list, lRI: thm, lRIq: thm, Gh: thm, Gh': thm} 
    1.20 +datatype rec_call_info = 
    1.21 +  RCInfo of {RI: thm, RIvs: (string * typ) list, lRI: thm, lRIq: thm, Gh: thm, Gh': thm} 
    1.22  
    1.23 -type clause_info =
    1.24 +datatype clause_info =
    1.25 +  ClauseInfo of 
    1.26       {
    1.27        no: int,
    1.28  
    1.29 @@ -72,11 +73,12 @@
    1.30       }
    1.31  
    1.32  
    1.33 -type curry_info =
    1.34 -     { argTs: typ list, curry_ss: simpset }
    1.35 +datatype curry_info =
    1.36 +  Curry of { argTs: typ list, curry_ss: simpset }
    1.37  
    1.38  
    1.39 -type prep_result =
    1.40 +datatype prep_result =
    1.41 +  Prep of
    1.42       {
    1.43        names: naming_context, 
    1.44        complete : term,
    1.45 @@ -84,7 +86,8 @@
    1.46        clauses: clause_info list
    1.47       }
    1.48  
    1.49 -type fundef_result =
    1.50 +datatype fundef_result =
    1.51 +  FundefResult of
    1.52       {
    1.53        f: term,
    1.54        G : term,
     2.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Fri May 05 22:11:19 2006 +0200
     2.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Sun May 07 00:00:13 2006 +0200
     2.3 @@ -26,19 +26,18 @@
     2.4  val True_implies = thm "True_implies"
     2.5  
     2.6  
     2.7 -(*#> FundefTermination.setup #> FundefDatatype.setup*)
     2.8 -
     2.9  fun fundef_afterqed congs curry_info name data natts thmss thy =
    2.10      let
    2.11  	val (complete_thm :: compat_thms) = map hd thmss
    2.12  	val fundef_data = FundefProof.mk_partial_rules_curried thy congs curry_info data (freezeT complete_thm) (map freezeT compat_thms)
    2.13 -	val {psimps, subset_pinduct, simple_pinduct, total_intro, dom_intros, ...} = fundef_data
    2.14 +	val FundefResult {psimps, subset_pinduct, simple_pinduct, total_intro, dom_intros, ...} = fundef_data
    2.15  
    2.16  	val (names, attsrcs) = split_list natts
    2.17  	val atts = map (map (Attrib.attribute thy)) attsrcs
    2.18  
    2.19 -	val accR = (#acc_R(#names(data)))
    2.20 -	val dom_abbrev = Logic.mk_equals (Free ("dom", fastype_of accR), accR)
    2.21 +	val Prep {names = Names {acc_R=accR, ...}, ...} = data
    2.22 +	val dom_abbrev = Logic.mk_equals (Free (name ^ "_dom", fastype_of accR), accR)
    2.23 +	val (_, thy) = LocalTheory.mapping NONE (Specification.abbreviation_i ("", false) [(NONE, dom_abbrev)]) thy
    2.24  
    2.25  	val thy = thy |> Theory.add_path name 
    2.26  
    2.27 @@ -46,7 +45,6 @@
    2.28  	val (_, thy) = PureThy.add_thms ((names ~~ psimps) ~~ atts) thy;
    2.29  	val thy = thy |> Theory.parent_path
    2.30  
    2.31 -	val (_, thy) = LocalTheory.mapping NONE (Specification.abbreviation_i ("", false) [(NONE, dom_abbrev)]) thy
    2.32  	val (_, thy) = PureThy.add_thms [(("cases", complete_thm), [RuleCases.case_names names])] thy
    2.33  	val (_, thy) = PureThy.add_thmss [(("domintros", dom_intros), [])] thy
    2.34  	val (_, thy) = PureThy.add_thms [(("termination", total_intro), [])] thy
    2.35 @@ -64,7 +62,7 @@
    2.36  	val congs = get_fundef_congs (Context.Theory thy)
    2.37  
    2.38  	val (curry_info, name, (data, thy)) = FundefPrep.prepare_fundef_curried congs (map (Sign.read_prop thy) eqns) thy
    2.39 -	val {complete, compat, ...} = data
    2.40 +	val Prep {complete, compat, ...} = data
    2.41  
    2.42  	val props = (complete :: compat) (*(complete :: fst (chop 110 compat))*)
    2.43      in
    2.44 @@ -78,7 +76,7 @@
    2.45      let
    2.46  	val totality = hd (hd thmss)
    2.47  
    2.48 -	val {psimps, simple_pinduct, ... }
    2.49 +	val FundefResult {psimps, simple_pinduct, ... }
    2.50  	  = the (get_fundef_data name thy)
    2.51  
    2.52  	val remove_domain_condition = full_simplify (HOL_basic_ss addsimps [totality, True_implies])
    2.53 @@ -133,7 +131,7 @@
    2.54  	val name = if name = "" then get_last_fundef thy else name
    2.55  	val data = the (get_fundef_data name thy)
    2.56  
    2.57 -	val {total_intro, ...} = data
    2.58 +	val FundefResult {total_intro, ...} = data
    2.59  	val goal = FundefTermination.mk_total_termination_goal data
    2.60      in
    2.61  	thy |> ProofContext.init
     3.1 --- a/src/HOL/Tools/function_package/fundef_prep.ML	Fri May 05 22:11:19 2006 +0200
     3.2 +++ b/src/HOL/Tools/function_package/fundef_prep.ML	Sun May 07 00:00:13 2006 +0200
     3.3 @@ -87,7 +87,7 @@
     3.4  
     3.5  fun mk_clause_info thy (names:naming_context) (no, (qs,gs,lhs,rhs)) (GI,tree) RIs =
     3.6      let
     3.7 -	val {domT, G, R, h, f, fvar, used, x, ...} = names
     3.8 +	val Names {domT, G, R, h, f, fvar, used, x, ...} = names
     3.9  				 
    3.10  	val zv = Var (("z",0), domT) (* for generating h_assums *)
    3.11  	val xv = Var (("x",0), domT)
    3.12 @@ -130,19 +130,20 @@
    3.13  		val Gh = assume (cterm_of thy Gh_term)
    3.14  		val Gh' = assume (cterm_of thy (rename_vars Gh_term))
    3.15  	    in
    3.16 -		{RI=RI, RIvs=RIvs, lRI=lRI, lRIq=lRIq, Gh=Gh, Gh'=Gh'}
    3.17 +		RCInfo {RI=RI, RIvs=RIvs, lRI=lRI, lRIq=lRIq, Gh=Gh, Gh'=Gh'}
    3.18  	    end
    3.19  
    3.20  	val case_hyp = assume (cterm_of thy (Trueprop (mk_eq (x, lhs))))
    3.21      in
    3.22 -	{
    3.23 -	 no=no,
    3.24 -	 qs=qs, gs=gs, lhs=lhs, rhs=rhs,		 
    3.25 -	 cqs=cqs, cvqs=cvqs, ags=ags,		 
    3.26 -	 cqs'=cqs', ags'=ags', lhs'=lhs', rhs'=rhs', ordcqs' = ordcqs',
    3.27 -	 GI=GI, lGI=lGI, RCs=map mk_call_info RIs,
    3.28 -	 tree=tree, case_hyp = case_hyp
    3.29 -	}
    3.30 +	ClauseInfo
    3.31 +	    {
    3.32 +	     no=no,
    3.33 +	     qs=qs, gs=gs, lhs=lhs, rhs=rhs,		 
    3.34 +	     cqs=cqs, cvqs=cvqs, ags=ags,		 
    3.35 +	     cqs'=cqs', ags'=ags', lhs'=lhs', rhs'=rhs', ordcqs' = ordcqs',
    3.36 +	     GI=GI, lGI=lGI, RCs=map mk_call_info RIs,
    3.37 +	     tree=tree, case_hyp = case_hyp
    3.38 +	    }
    3.39      end
    3.40  
    3.41  
    3.42 @@ -191,7 +192,7 @@
    3.43  
    3.44  	val ([f_def], thy) = PureThy.add_defs_i false [((fxname ^ "_def", f_eq), [])] thy
    3.45      in
    3.46 -	({f=f, glrs=glrs, glrs'=glrs', fvar=fvar, fvarname=fvarname, domT=domT, ranT=ranT, G=G, R=R, acc_R=acc_R, h=h, x=x, y=y, z=z, a=a, D=D, P=P, Pbool=Pbool, f_def=f_def, used=allused, trees=trees}, thy)
    3.47 +	(Names {f=f, glrs=glrs, glrs'=glrs', fvar=fvar, fvarname=fvarname, domT=domT, ranT=ranT, G=G, R=R, acc_R=acc_R, h=h, x=x, y=y, z=z, a=a, D=D, P=P, Pbool=Pbool, f_def=f_def, used=allused, trees=trees}, thy)
    3.48      end
    3.49  
    3.50  
    3.51 @@ -222,7 +223,7 @@
    3.52  
    3.53  fun mk_GIntro thy names (qs, gs, lhs, rhs) Ris =
    3.54      let
    3.55 -	val { domT, R, G, f, fvar, h, y, Pbool, ... } = names
    3.56 +	val Names { domT, R, G, f, fvar, h, y, Pbool, ... } = names
    3.57  
    3.58  	val z = Var (("z",0), domT)
    3.59  	val x = Var (("x",0), domT)
    3.60 @@ -241,7 +242,7 @@
    3.61  
    3.62  fun mk_completeness names glrs =
    3.63      let
    3.64 -	val {domT, x, Pbool, ...} = names
    3.65 +	val Names {domT, x, Pbool, ...} = names
    3.66  
    3.67  	fun mk_case (qs, gs, lhs, _) = Trueprop Pbool
    3.68  						|> curry Logic.mk_implies (Trueprop (mk_eq (x, lhs)))
    3.69 @@ -255,7 +256,7 @@
    3.70  
    3.71  fun extract_conditions thy names trees congs =
    3.72      let
    3.73 -	val {f, G, R, acc_R, domT, ranT, f_def, x, z, fvarname, glrs, glrs', ...} = names
    3.74 +	val Names {f, G, R, acc_R, domT, ranT, f_def, x, z, fvarname, glrs, glrs', ...} = names
    3.75  
    3.76  	val (vRiss, preRiss, Riss) = split_list3 (map2 (extract_Ris thy congs f R) trees glrs)
    3.77  	val Gis = map2 (mk_GIntro thy names) glrs preRiss
    3.78 @@ -294,7 +295,7 @@
    3.79  fun prepare_fundef congs eqs fname thy =
    3.80      let
    3.81  	val (names, thy) = setup_context (analyze_eqs eqs) fname congs thy
    3.82 -	val {G, R, glrs, trees, ...} = names
    3.83 +	val Names {G, R, glrs, trees, ...} = names
    3.84  
    3.85  	val {G_intros, vRiss, R_intross, complete, compat} = extract_conditions thy names trees congs
    3.86  
    3.87 @@ -304,7 +305,7 @@
    3.88  	val n = length glrs
    3.89  	val clauses = map3 (mk_clause_info thy names) ((1 upto n) ~~ glrs) (G_intro_thms ~~ trees) (map2 (curry op ~~) vRiss R_intro_thmss)
    3.90      in
    3.91 -	({names = names, complete=complete, compat=compat, clauses = clauses},
    3.92 +	(Prep {names = names, complete=complete, compat=compat, clauses = clauses},
    3.93  	 thy) 
    3.94      end
    3.95  
    3.96 @@ -346,7 +347,7 @@
    3.97  		val g_to_f_ss = HOL_basic_ss addsimps [symmetric f_def]
    3.98  		val eqs_tupled = map (Pattern.rewrite_term thy [(f, f_lambda)] []) eqs
    3.99  	    in
   3.100 -		(SOME {curry_ss = g_to_f_ss, argTs = caTs}, fxname, prepare_fundef congs eqs_tupled fxname thy)
   3.101 +		(SOME (Curry {curry_ss = g_to_f_ss, argTs = caTs}), fxname, prepare_fundef congs eqs_tupled fxname thy)
   3.102  	    end
   3.103      end
   3.104  
     4.1 --- a/src/HOL/Tools/function_package/fundef_proof.ML	Fri May 05 22:11:19 2006 +0200
     4.2 +++ b/src/HOL/Tools/function_package/fundef_proof.ML	Sun May 07 00:00:13 2006 +0200
     4.3 @@ -42,10 +42,10 @@
     4.4  
     4.5  
     4.6      
     4.7 -fun mk_simp thy (names:naming_context) f_iff graph_is_function clause valthm =
     4.8 +fun mk_simp thy names f_iff graph_is_function clause valthm =
     4.9      let
    4.10 -	val {R, acc_R, domT, z, ...} = names
    4.11 -	val {qs, cqs, gs, lhs, rhs, ...} = clause
    4.12 +	val Names {R, acc_R, domT, z, ...} = names
    4.13 +	val ClauseInfo {qs, cqs, gs, lhs, rhs, ...} = clause
    4.14  	val lhs_acc = cterm_of thy (Trueprop (mk_mem (lhs, acc_R))) (* "lhs : acc R" *)
    4.15  	val z_smaller = cterm_of thy (Trueprop (mk_relmemT domT domT (z, lhs) R)) (* "(z, lhs) : R" *)
    4.16      in
    4.17 @@ -65,9 +65,9 @@
    4.18  
    4.19  
    4.20  
    4.21 -fun mk_partial_induct_rule thy (names:naming_context) complete_thm clauses =
    4.22 +fun mk_partial_induct_rule thy names complete_thm clauses =
    4.23      let
    4.24 -	val {domT, R, acc_R, x, z, a, P, D, ...} = names
    4.25 +	val Names {domT, R, acc_R, x, z, a, P, D, ...} = names
    4.26  
    4.27  	val x_D = assume (cterm_of thy (Trueprop (mk_mem (x, D))))
    4.28  	val a_D = cterm_of thy (Trueprop (mk_mem (a, D)))
    4.29 @@ -92,14 +92,14 @@
    4.30  
    4.31  	fun prove_case clause =
    4.32  	    let
    4.33 -		val {qs, cqs, ags, gs, lhs, rhs, case_hyp, RCs, ...} = clause
    4.34 +		val ClauseInfo {qs, cqs, ags, gs, lhs, rhs, case_hyp, RCs, ...} = clause
    4.35  								       
    4.36  		val replace_x_ss = HOL_basic_ss addsimps [case_hyp]
    4.37  		val lhs_D = simplify replace_x_ss x_D (* lhs : D *)
    4.38  		val sih = full_simplify replace_x_ss aihyp
    4.39  					
    4.40  					(* FIXME: Variable order destroyed by forall_intr_vars *)
    4.41 -		val P_recs = map (fn {lRI, RIvs, ...} => (lRI RS sih) |> forall_intr_vars) RCs   (*  [P rec1, P rec2, ... ]  *)
    4.42 +		val P_recs = map (fn RCInfo {lRI, RIvs, ...} => (lRI RS sih) |> forall_intr_vars) RCs   (*  [P rec1, P rec2, ... ]  *)
    4.43  			     
    4.44  		val step = Trueprop (P $ lhs)
    4.45  				    |> fold_rev (curry Logic.mk_implies o prop_of) P_recs
    4.46 @@ -183,16 +183,16 @@
    4.47  
    4.48  
    4.49  (* recover the order of Vars *)
    4.50 -fun get_var_order thy (clauses: clause_info list) =
    4.51 -    map (fn ({cqs,...}, {cqs',...}) => map (cterm_of thy o free_to_var o term_of) (cqs @ cqs')) (upairs clauses)
    4.52 +fun get_var_order thy clauses =
    4.53 +    map (fn (ClauseInfo {cqs,...}, ClauseInfo {cqs',...}) => map (cterm_of thy o free_to_var o term_of) (cqs @ cqs')) (upairs clauses)
    4.54  
    4.55  
    4.56  (* Returns "Gsi, Gsj', lhs_i = lhs_j' |-- rhs_j'_f = rhs_i_f" *)
    4.57  (* if j < i, then turn around *)
    4.58  fun get_compat_thm thy cts clausei clausej =
    4.59      let 
    4.60 -	val {no=i, cqs=qsi, ags=gsi, lhs=lhsi, ...} = clausei
    4.61 -	val {no=j, cqs'=qsj', ags'=gsj', lhs'=lhsj', ...} = clausej
    4.62 +	val ClauseInfo {no=i, cqs=qsi, ags=gsi, lhs=lhsi, ...} = clausei
    4.63 +	val ClauseInfo {no=j, cqs'=qsj', ags'=gsj', lhs'=lhsj', ...} = clausej
    4.64  
    4.65  	val lhsi_eq_lhsj' = cterm_of thy (Trueprop (mk_eq (lhsi, lhsj')))
    4.66      in if j < i then
    4.67 @@ -227,14 +227,14 @@
    4.68  here. *)
    4.69  fun mk_replacement_lemma thy (names:naming_context) ih_elim clause = 
    4.70      let 
    4.71 -	val {fvar, f, x, y, h, Pbool, G, ranT, domT, R, ...} = names 
    4.72 -	val {qs,cqs,ags,lhs,rhs,cqs',ags',case_hyp, RCs, tree, ...} = clause
    4.73 +	val Names {fvar, f, x, y, h, Pbool, G, ranT, domT, R, ...} = names 
    4.74 +	val ClauseInfo {qs,cqs,ags,lhs,rhs,cqs',ags',case_hyp, RCs, tree, ...} = clause
    4.75  
    4.76  	val ih_elim_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ih_elim
    4.77  
    4.78 -	val Ris = map #lRIq RCs
    4.79 -	val h_assums = map #Gh RCs
    4.80 -	val h_assums' = map #Gh' RCs
    4.81 +	val Ris = map (fn RCInfo {lRIq, ...} => lRIq) RCs
    4.82 +	val h_assums = map (fn RCInfo {Gh, ...} => Gh) RCs
    4.83 +	val h_assums' = map (fn RCInfo {Gh', ...} => Gh') RCs
    4.84  
    4.85  	val ih_elim_case_inst = instantiate' [] [NONE, SOME (cterm_of thy h)] ih_elim_case (* Should be done globally *)
    4.86  
    4.87 @@ -255,15 +255,15 @@
    4.88  
    4.89  
    4.90  
    4.91 -fun mk_uniqueness_clause thy (names:naming_context) compat_store (clausei:clause_info) (clausej:clause_info) RLj =
    4.92 +fun mk_uniqueness_clause thy names compat_store clausei clausej RLj =
    4.93      let
    4.94 -	val {f, h, y, ...} = names
    4.95 -	val {no=i, lhs=lhsi, case_hyp, ...} = clausei
    4.96 -	val {no=j, ags'=gsj', lhs'=lhsj', rhs'=rhsj', RCs=RCsj, ordcqs'=ordcqs'j, ...} = clausej
    4.97 +	val Names {f, h, y, ...} = names
    4.98 +	val ClauseInfo {no=i, lhs=lhsi, case_hyp, ...} = clausei
    4.99 +	val ClauseInfo {no=j, ags'=gsj', lhs'=lhsj', rhs'=rhsj', RCs=RCsj, ordcqs'=ordcqs'j, ...} = clausej
   4.100  
   4.101  	val rhsj'h = Pattern.rewrite_term thy [(f,h)] [] rhsj'
   4.102  	val compat = get_compat_thm thy compat_store clausei clausej
   4.103 -	val Ghsj' = map (fn {Gh', ...} => Gh') RCsj
   4.104 +	val Ghsj' = map (fn RCInfo {Gh', ...} => Gh') RCsj
   4.105  
   4.106  	val y_eq_rhsj'h = assume (cterm_of thy (Trueprop (mk_eq (y, rhsj'h))))
   4.107  	val lhsi_eq_lhsj' = assume (cterm_of thy (Trueprop (mk_eq (lhsi, lhsj')))) (* lhs_i = lhs_j' |-- lhs_i = lhs_j'	*)
   4.108 @@ -286,17 +286,17 @@
   4.109  
   4.110  
   4.111  
   4.112 -fun mk_uniqueness_case thy (names:naming_context) ihyp ih_intro G_cases compat_store clauses rep_lemmas (clausei:clause_info) =
   4.113 +fun mk_uniqueness_case thy names ihyp ih_intro G_cases compat_store clauses rep_lemmas clausei =
   4.114      let
   4.115 -	val {x, y, G, fvar, f, ranT, ...} = names
   4.116 -	val {lhs, rhs, qs, cqs, ags, case_hyp, lGI, RCs, ...} = clausei
   4.117 +	val Names {x, y, G, fvar, f, ranT, ...} = names
   4.118 +	val ClauseInfo {lhs, rhs, qs, cqs, ags, case_hyp, lGI, RCs, ...} = clausei
   4.119  
   4.120  	val ih_intro_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ih_intro
   4.121  
   4.122 -	fun prep_RC ({lRIq,RIvs, ...} : rec_call_info) = lRIq
   4.123 -							     |> fold (forall_elim o cterm_of thy o Free) RIvs
   4.124 -							     |> (fn it => it RS ih_intro_case)
   4.125 -							     |> fold_rev (forall_intr o cterm_of thy o Free) RIvs
   4.126 +	fun prep_RC (RCInfo {lRIq,RIvs, ...}) = lRIq
   4.127 +						    |> fold (forall_elim o cterm_of thy o Free) RIvs
   4.128 +						    |> (fn it => it RS ih_intro_case)
   4.129 +						    |> fold_rev (forall_intr o cterm_of thy o Free) RIvs
   4.130  
   4.131  	val existence = lGI |> instantiate ([], [(cterm_of thy (free_to_var fvar), cterm_of thy f)])
   4.132  			    |> fold (curry op COMP o prep_RC) RCs 
   4.133 @@ -340,10 +340,10 @@
   4.134  
   4.135  
   4.136  (* Does this work with Guards??? *)
   4.137 -fun mk_domain_intro thy (names:naming_context) R_cases clause =
   4.138 +fun mk_domain_intro thy names R_cases clause =
   4.139      let
   4.140 -	val {z, R, acc_R, ...} = names
   4.141 -	val {qs, gs, lhs, rhs, ...} = clause
   4.142 +	val Names {z, R, acc_R, ...} = names
   4.143 +	val ClauseInfo {qs, gs, lhs, rhs, ...} = clause
   4.144  
   4.145  	val z_lhs = cterm_of thy (HOLogic.mk_prod (z,lhs))
   4.146  	val z_acc = cterm_of thy (HOLogic.mk_mem (z,acc_R))
   4.147 @@ -368,10 +368,10 @@
   4.148  
   4.149  
   4.150  
   4.151 -fun mk_nest_term_case thy (names:naming_context) R' ihyp clause =
   4.152 +fun mk_nest_term_case thy names R' ihyp clause =
   4.153      let
   4.154 -	val {x, z, ...} = names
   4.155 -	val {qs,cqs,ags,lhs,rhs,tree,case_hyp,...} = clause
   4.156 +	val Names {x, z, ...} = names
   4.157 +	val ClauseInfo {qs,cqs,ags,lhs,rhs,tree,case_hyp,...} = clause
   4.158  
   4.159  	val ih_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ihyp
   4.160  
   4.161 @@ -421,9 +421,9 @@
   4.162      end
   4.163  
   4.164  
   4.165 -fun mk_nest_term_rule thy (names:naming_context) clauses =
   4.166 +fun mk_nest_term_rule thy names clauses =
   4.167      let
   4.168 -	val { R, acc_R, domT, x, z, ... } = names
   4.169 +	val Names { R, acc_R, domT, x, z, ... } = names
   4.170  
   4.171  	val R_elim = hd (#elims (snd (the (InductivePackage.get_inductive thy (fst (dest_Const R))))))
   4.172  
   4.173 @@ -469,8 +469,8 @@
   4.174  
   4.175  fun mk_partial_rules thy congs data complete_thm compat_thms =
   4.176      let
   4.177 -	val {names, clauses, complete, compat, ...} = data
   4.178 -	val {G, R, acc_R, domT, ranT, f, f_def, x, z, fvarname, ...}:naming_context = names
   4.179 +	val Prep {names, clauses, complete, compat, ...} = data
   4.180 +	val Names {G, R, acc_R, domT, ranT, f, f_def, x, z, fvarname, ...}:naming_context = names
   4.181  
   4.182  (*	val _ = Output.debug "closing derivation: completeness"
   4.183  	val _ = Output.debug (Proofterm.size_of_proof (proof_of complete_thm))
   4.184 @@ -541,7 +541,7 @@
   4.185  	val _ = Output.debug "Proving domain introduction rules"
   4.186  	val dom_intros = map (mk_domain_intro thy names R_cases) clauses
   4.187      in 
   4.188 -	{f=f, G=G, R=R, compatibility=compat_thms, completeness=complete_thm, 
   4.189 +	FundefResult {f=f, G=G, R=R, compatibility=compat_thms, completeness=complete_thm, 
   4.190  	 psimps=psimps, subset_pinduct=subset_pinduct, simple_pinduct=simple_pinduct, total_intro=total_intro,
   4.191  	 dom_intros=dom_intros}
   4.192      end
   4.193 @@ -566,9 +566,9 @@
   4.194  
   4.195  fun mk_partial_rules_curried thy congs NONE data complete_thm compat_thms =
   4.196      mk_partial_rules thy congs data complete_thm compat_thms 
   4.197 -  | mk_partial_rules_curried thy congs (SOME {curry_ss, argTs}) data complete_thm compat_thms =
   4.198 +  | mk_partial_rules_curried thy congs (SOME (Curry {curry_ss, argTs})) data complete_thm compat_thms =
   4.199      let
   4.200 -	val {f, G, R, compatibility, completeness, psimps, subset_pinduct,simple_pinduct,total_intro,dom_intros} =
   4.201 +	val FundefResult {f, G, R, compatibility, completeness, psimps, subset_pinduct,simple_pinduct,total_intro,dom_intros} =
   4.202  	    mk_partial_rules thy congs data complete_thm compat_thms 
   4.203  	val cpsimps = map (simplify curry_ss) psimps
   4.204  	val cpinduct = full_simplify curry_ss simple_pinduct
   4.205 @@ -576,7 +576,7 @@
   4.206  	val cdom_intros = map (full_simplify curry_ss) dom_intros
   4.207  	val ctotal_intro = full_simplify curry_ss total_intro
   4.208      in
   4.209 -	{f=f, G=G, R=R, compatibility=compat_thms, completeness=complete_thm, 
   4.210 +	FundefResult {f=f, G=G, R=R, compatibility=compat_thms, completeness=complete_thm, 
   4.211  	 psimps=cpsimps, subset_pinduct=subset_pinduct, simple_pinduct=cpinduct, total_intro=ctotal_intro, dom_intros=cdom_intros}
   4.212      end
   4.213  
     5.1 --- a/src/HOL/Tools/function_package/termination.ML	Fri May 05 22:11:19 2006 +0200
     5.2 +++ b/src/HOL/Tools/function_package/termination.ML	Sun May 07 00:00:13 2006 +0200
     5.3 @@ -20,9 +20,9 @@
     5.4  open FundefCommon
     5.5  open FundefAbbrev
     5.6  
     5.7 -fun mk_total_termination_goal (data: fundef_result) =
     5.8 +fun mk_total_termination_goal data =
     5.9      let
    5.10 -	val {R, f, ... } = data
    5.11 +	val FundefResult {R, f, ... } = data
    5.12  
    5.13  	val domT = domain_type (fastype_of f)
    5.14  	val x = Free ("x", domT)
    5.15 @@ -30,9 +30,9 @@
    5.16  	Trueprop (mk_mem (x, Const (acc_const_name, fastype_of R --> HOLogic.mk_setT domT) $ R))
    5.17      end
    5.18  
    5.19 -fun mk_partial_termination_goal thy (data: fundef_result) dom =
    5.20 +fun mk_partial_termination_goal thy data dom =
    5.21      let
    5.22 -	val {R, f, ... } = data
    5.23 +	val FundefResult {R, f, ... } = data
    5.24  
    5.25  	val domT = domain_type (fastype_of f)
    5.26  	val D = Sign.simple_read_term thy (Type.varifyT (HOLogic.mk_setT domT)) dom
     6.1 --- a/src/HOL/ex/Fundefs.thy	Fri May 05 22:11:19 2006 +0200
     6.2 +++ b/src/HOL/ex/Fundefs.thy	Sun May 07 00:00:13 2006 +0200
     6.3 @@ -58,7 +58,7 @@
     6.4  by pat_completeness auto
     6.5  
     6.6  lemma nz_is_zero: (* A lemma we need to prove termination *)
     6.7 -  assumes trm: "x \<in> nz.dom"
     6.8 +  assumes trm: "x \<in> nz_dom"
     6.9    shows "nz x = 0"
    6.10  using trm
    6.11  by induct auto