# HG changeset patch
# User krauss
# Date 1146952813 -7200
# Node ID c5fa77b03442ab550d67b8a33e8702c793db470d
# Parent  a669c98b9c24ff27c88c01d09680f420a6e1a642
function-package: Changed record usage to make sml/nj happy...

diff -r a669c98b9c24 -r c5fa77b03442 src/HOL/Tools/function_package/fundef_common.ML
--- a/src/HOL/Tools/function_package/fundef_common.ML	Fri May 05 22:11:19 2006 +0200
+++ b/src/HOL/Tools/function_package/fundef_common.ML	Sun May 07 00:00:13 2006 +0200
@@ -29,8 +29,8 @@
 
 (* A record containing all the relevant symbols and types needed during the proof.
    This is set up at the beginning and does not change. *)
-type naming_context =
-     { f: term, fvarname: string, fvar: term, domT: typ, ranT: typ,
+datatype naming_context =
+   Names of { f: term, fvarname: string, fvar: term, domT: typ, ranT: typ,
        G: term, R: term, acc_R: term, h: term, y: term, x: term, z: term, a:term, P: term, 
        D: term, Pbool:term,
        glrs: (term list * term list * term * term) list,
@@ -41,10 +41,11 @@
      }
 
 
-type rec_call_info = 
-     {RI: thm, RIvs: (string * typ) list, lRI: thm, lRIq: thm, Gh: thm, Gh': thm} 
+datatype rec_call_info = 
+  RCInfo of {RI: thm, RIvs: (string * typ) list, lRI: thm, lRIq: thm, Gh: thm, Gh': thm} 
 
-type clause_info =
+datatype clause_info =
+  ClauseInfo of 
      {
       no: int,
 
@@ -72,11 +73,12 @@
      }
 
 
-type curry_info =
-     { argTs: typ list, curry_ss: simpset }
+datatype curry_info =
+  Curry of { argTs: typ list, curry_ss: simpset }
 
 
-type prep_result =
+datatype prep_result =
+  Prep of
      {
       names: naming_context, 
       complete : term,
@@ -84,7 +86,8 @@
       clauses: clause_info list
      }
 
-type fundef_result =
+datatype fundef_result =
+  FundefResult of
      {
       f: term,
       G : term,
diff -r a669c98b9c24 -r c5fa77b03442 src/HOL/Tools/function_package/fundef_package.ML
--- a/src/HOL/Tools/function_package/fundef_package.ML	Fri May 05 22:11:19 2006 +0200
+++ b/src/HOL/Tools/function_package/fundef_package.ML	Sun May 07 00:00:13 2006 +0200
@@ -26,19 +26,18 @@
 val True_implies = thm "True_implies"
 
 
-(*#> FundefTermination.setup #> FundefDatatype.setup*)
-
 fun fundef_afterqed congs curry_info name data natts thmss thy =
     let
 	val (complete_thm :: compat_thms) = map hd thmss
 	val fundef_data = FundefProof.mk_partial_rules_curried thy congs curry_info data (freezeT complete_thm) (map freezeT compat_thms)
-	val {psimps, subset_pinduct, simple_pinduct, total_intro, dom_intros, ...} = fundef_data
+	val FundefResult {psimps, subset_pinduct, simple_pinduct, total_intro, dom_intros, ...} = fundef_data
 
 	val (names, attsrcs) = split_list natts
 	val atts = map (map (Attrib.attribute thy)) attsrcs
 
-	val accR = (#acc_R(#names(data)))
-	val dom_abbrev = Logic.mk_equals (Free ("dom", fastype_of accR), accR)
+	val Prep {names = Names {acc_R=accR, ...}, ...} = data
+	val dom_abbrev = Logic.mk_equals (Free (name ^ "_dom", fastype_of accR), accR)
+	val (_, thy) = LocalTheory.mapping NONE (Specification.abbreviation_i ("", false) [(NONE, dom_abbrev)]) thy
 
 	val thy = thy |> Theory.add_path name 
 
@@ -46,7 +45,6 @@
 	val (_, thy) = PureThy.add_thms ((names ~~ psimps) ~~ atts) thy;
 	val thy = thy |> Theory.parent_path
 
-	val (_, thy) = LocalTheory.mapping NONE (Specification.abbreviation_i ("", false) [(NONE, dom_abbrev)]) thy
 	val (_, thy) = PureThy.add_thms [(("cases", complete_thm), [RuleCases.case_names names])] thy
 	val (_, thy) = PureThy.add_thmss [(("domintros", dom_intros), [])] thy
 	val (_, thy) = PureThy.add_thms [(("termination", total_intro), [])] thy
@@ -64,7 +62,7 @@
 	val congs = get_fundef_congs (Context.Theory thy)
 
 	val (curry_info, name, (data, thy)) = FundefPrep.prepare_fundef_curried congs (map (Sign.read_prop thy) eqns) thy
-	val {complete, compat, ...} = data
+	val Prep {complete, compat, ...} = data
 
 	val props = (complete :: compat) (*(complete :: fst (chop 110 compat))*)
     in
@@ -78,7 +76,7 @@
     let
 	val totality = hd (hd thmss)
 
-	val {psimps, simple_pinduct, ... }
+	val FundefResult {psimps, simple_pinduct, ... }
 	  = the (get_fundef_data name thy)
 
 	val remove_domain_condition = full_simplify (HOL_basic_ss addsimps [totality, True_implies])
@@ -133,7 +131,7 @@
 	val name = if name = "" then get_last_fundef thy else name
 	val data = the (get_fundef_data name thy)
 
-	val {total_intro, ...} = data
+	val FundefResult {total_intro, ...} = data
 	val goal = FundefTermination.mk_total_termination_goal data
     in
 	thy |> ProofContext.init
diff -r a669c98b9c24 -r c5fa77b03442 src/HOL/Tools/function_package/fundef_prep.ML
--- a/src/HOL/Tools/function_package/fundef_prep.ML	Fri May 05 22:11:19 2006 +0200
+++ b/src/HOL/Tools/function_package/fundef_prep.ML	Sun May 07 00:00:13 2006 +0200
@@ -87,7 +87,7 @@
 
 fun mk_clause_info thy (names:naming_context) (no, (qs,gs,lhs,rhs)) (GI,tree) RIs =
     let
-	val {domT, G, R, h, f, fvar, used, x, ...} = names
+	val Names {domT, G, R, h, f, fvar, used, x, ...} = names
 				 
 	val zv = Var (("z",0), domT) (* for generating h_assums *)
 	val xv = Var (("x",0), domT)
@@ -130,19 +130,20 @@
 		val Gh = assume (cterm_of thy Gh_term)
 		val Gh' = assume (cterm_of thy (rename_vars Gh_term))
 	    in
-		{RI=RI, RIvs=RIvs, lRI=lRI, lRIq=lRIq, Gh=Gh, Gh'=Gh'}
+		RCInfo {RI=RI, RIvs=RIvs, lRI=lRI, lRIq=lRIq, Gh=Gh, Gh'=Gh'}
 	    end
 
 	val case_hyp = assume (cterm_of thy (Trueprop (mk_eq (x, lhs))))
     in
-	{
-	 no=no,
-	 qs=qs, gs=gs, lhs=lhs, rhs=rhs,		 
-	 cqs=cqs, cvqs=cvqs, ags=ags,		 
-	 cqs'=cqs', ags'=ags', lhs'=lhs', rhs'=rhs', ordcqs' = ordcqs',
-	 GI=GI, lGI=lGI, RCs=map mk_call_info RIs,
-	 tree=tree, case_hyp = case_hyp
-	}
+	ClauseInfo
+	    {
+	     no=no,
+	     qs=qs, gs=gs, lhs=lhs, rhs=rhs,		 
+	     cqs=cqs, cvqs=cvqs, ags=ags,		 
+	     cqs'=cqs', ags'=ags', lhs'=lhs', rhs'=rhs', ordcqs' = ordcqs',
+	     GI=GI, lGI=lGI, RCs=map mk_call_info RIs,
+	     tree=tree, case_hyp = case_hyp
+	    }
     end
 
 
@@ -191,7 +192,7 @@
 
 	val ([f_def], thy) = PureThy.add_defs_i false [((fxname ^ "_def", f_eq), [])] thy
     in
-	({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)
+	(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)
     end
 
 
@@ -222,7 +223,7 @@
 
 fun mk_GIntro thy names (qs, gs, lhs, rhs) Ris =
     let
-	val { domT, R, G, f, fvar, h, y, Pbool, ... } = names
+	val Names { domT, R, G, f, fvar, h, y, Pbool, ... } = names
 
 	val z = Var (("z",0), domT)
 	val x = Var (("x",0), domT)
@@ -241,7 +242,7 @@
 
 fun mk_completeness names glrs =
     let
-	val {domT, x, Pbool, ...} = names
+	val Names {domT, x, Pbool, ...} = names
 
 	fun mk_case (qs, gs, lhs, _) = Trueprop Pbool
 						|> curry Logic.mk_implies (Trueprop (mk_eq (x, lhs)))
@@ -255,7 +256,7 @@
 
 fun extract_conditions thy names trees congs =
     let
-	val {f, G, R, acc_R, domT, ranT, f_def, x, z, fvarname, glrs, glrs', ...} = names
+	val Names {f, G, R, acc_R, domT, ranT, f_def, x, z, fvarname, glrs, glrs', ...} = names
 
 	val (vRiss, preRiss, Riss) = split_list3 (map2 (extract_Ris thy congs f R) trees glrs)
 	val Gis = map2 (mk_GIntro thy names) glrs preRiss
@@ -294,7 +295,7 @@
 fun prepare_fundef congs eqs fname thy =
     let
 	val (names, thy) = setup_context (analyze_eqs eqs) fname congs thy
-	val {G, R, glrs, trees, ...} = names
+	val Names {G, R, glrs, trees, ...} = names
 
 	val {G_intros, vRiss, R_intross, complete, compat} = extract_conditions thy names trees congs
 
@@ -304,7 +305,7 @@
 	val n = length glrs
 	val clauses = map3 (mk_clause_info thy names) ((1 upto n) ~~ glrs) (G_intro_thms ~~ trees) (map2 (curry op ~~) vRiss R_intro_thmss)
     in
-	({names = names, complete=complete, compat=compat, clauses = clauses},
+	(Prep {names = names, complete=complete, compat=compat, clauses = clauses},
 	 thy) 
     end
 
@@ -346,7 +347,7 @@
 		val g_to_f_ss = HOL_basic_ss addsimps [symmetric f_def]
 		val eqs_tupled = map (Pattern.rewrite_term thy [(f, f_lambda)] []) eqs
 	    in
-		(SOME {curry_ss = g_to_f_ss, argTs = caTs}, fxname, prepare_fundef congs eqs_tupled fxname thy)
+		(SOME (Curry {curry_ss = g_to_f_ss, argTs = caTs}), fxname, prepare_fundef congs eqs_tupled fxname thy)
 	    end
     end
 
diff -r a669c98b9c24 -r c5fa77b03442 src/HOL/Tools/function_package/fundef_proof.ML
--- a/src/HOL/Tools/function_package/fundef_proof.ML	Fri May 05 22:11:19 2006 +0200
+++ b/src/HOL/Tools/function_package/fundef_proof.ML	Sun May 07 00:00:13 2006 +0200
@@ -42,10 +42,10 @@
 
 
     
-fun mk_simp thy (names:naming_context) f_iff graph_is_function clause valthm =
+fun mk_simp thy names f_iff graph_is_function clause valthm =
     let
-	val {R, acc_R, domT, z, ...} = names
-	val {qs, cqs, gs, lhs, rhs, ...} = clause
+	val Names {R, acc_R, domT, z, ...} = names
+	val ClauseInfo {qs, cqs, gs, lhs, rhs, ...} = clause
 	val lhs_acc = cterm_of thy (Trueprop (mk_mem (lhs, acc_R))) (* "lhs : acc R" *)
 	val z_smaller = cterm_of thy (Trueprop (mk_relmemT domT domT (z, lhs) R)) (* "(z, lhs) : R" *)
     in
@@ -65,9 +65,9 @@
 
 
 
-fun mk_partial_induct_rule thy (names:naming_context) complete_thm clauses =
+fun mk_partial_induct_rule thy names complete_thm clauses =
     let
-	val {domT, R, acc_R, x, z, a, P, D, ...} = names
+	val Names {domT, R, acc_R, x, z, a, P, D, ...} = names
 
 	val x_D = assume (cterm_of thy (Trueprop (mk_mem (x, D))))
 	val a_D = cterm_of thy (Trueprop (mk_mem (a, D)))
@@ -92,14 +92,14 @@
 
 	fun prove_case clause =
 	    let
-		val {qs, cqs, ags, gs, lhs, rhs, case_hyp, RCs, ...} = clause
+		val ClauseInfo {qs, cqs, ags, gs, lhs, rhs, case_hyp, RCs, ...} = clause
 								       
 		val replace_x_ss = HOL_basic_ss addsimps [case_hyp]
 		val lhs_D = simplify replace_x_ss x_D (* lhs : D *)
 		val sih = full_simplify replace_x_ss aihyp
 					
 					(* FIXME: Variable order destroyed by forall_intr_vars *)
-		val P_recs = map (fn {lRI, RIvs, ...} => (lRI RS sih) |> forall_intr_vars) RCs   (*  [P rec1, P rec2, ... ]  *)
+		val P_recs = map (fn RCInfo {lRI, RIvs, ...} => (lRI RS sih) |> forall_intr_vars) RCs   (*  [P rec1, P rec2, ... ]  *)
 			     
 		val step = Trueprop (P $ lhs)
 				    |> fold_rev (curry Logic.mk_implies o prop_of) P_recs
@@ -183,16 +183,16 @@
 
 
 (* recover the order of Vars *)
-fun get_var_order thy (clauses: clause_info list) =
-    map (fn ({cqs,...}, {cqs',...}) => map (cterm_of thy o free_to_var o term_of) (cqs @ cqs')) (upairs clauses)
+fun get_var_order thy clauses =
+    map (fn (ClauseInfo {cqs,...}, ClauseInfo {cqs',...}) => map (cterm_of thy o free_to_var o term_of) (cqs @ cqs')) (upairs clauses)
 
 
 (* Returns "Gsi, Gsj', lhs_i = lhs_j' |-- rhs_j'_f = rhs_i_f" *)
 (* if j < i, then turn around *)
 fun get_compat_thm thy cts clausei clausej =
     let 
-	val {no=i, cqs=qsi, ags=gsi, lhs=lhsi, ...} = clausei
-	val {no=j, cqs'=qsj', ags'=gsj', lhs'=lhsj', ...} = clausej
+	val ClauseInfo {no=i, cqs=qsi, ags=gsi, lhs=lhsi, ...} = clausei
+	val ClauseInfo {no=j, cqs'=qsj', ags'=gsj', lhs'=lhsj', ...} = clausej
 
 	val lhsi_eq_lhsj' = cterm_of thy (Trueprop (mk_eq (lhsi, lhsj')))
     in if j < i then
@@ -227,14 +227,14 @@
 here. *)
 fun mk_replacement_lemma thy (names:naming_context) ih_elim clause = 
     let 
-	val {fvar, f, x, y, h, Pbool, G, ranT, domT, R, ...} = names 
-	val {qs,cqs,ags,lhs,rhs,cqs',ags',case_hyp, RCs, tree, ...} = clause
+	val Names {fvar, f, x, y, h, Pbool, G, ranT, domT, R, ...} = names 
+	val ClauseInfo {qs,cqs,ags,lhs,rhs,cqs',ags',case_hyp, RCs, tree, ...} = clause
 
 	val ih_elim_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ih_elim
 
-	val Ris = map #lRIq RCs
-	val h_assums = map #Gh RCs
-	val h_assums' = map #Gh' RCs
+	val Ris = map (fn RCInfo {lRIq, ...} => lRIq) RCs
+	val h_assums = map (fn RCInfo {Gh, ...} => Gh) RCs
+	val h_assums' = map (fn RCInfo {Gh', ...} => Gh') RCs
 
 	val ih_elim_case_inst = instantiate' [] [NONE, SOME (cterm_of thy h)] ih_elim_case (* Should be done globally *)
 
@@ -255,15 +255,15 @@
 
 
 
-fun mk_uniqueness_clause thy (names:naming_context) compat_store (clausei:clause_info) (clausej:clause_info) RLj =
+fun mk_uniqueness_clause thy names compat_store clausei clausej RLj =
     let
-	val {f, h, y, ...} = names
-	val {no=i, lhs=lhsi, case_hyp, ...} = clausei
-	val {no=j, ags'=gsj', lhs'=lhsj', rhs'=rhsj', RCs=RCsj, ordcqs'=ordcqs'j, ...} = clausej
+	val Names {f, h, y, ...} = names
+	val ClauseInfo {no=i, lhs=lhsi, case_hyp, ...} = clausei
+	val ClauseInfo {no=j, ags'=gsj', lhs'=lhsj', rhs'=rhsj', RCs=RCsj, ordcqs'=ordcqs'j, ...} = clausej
 
 	val rhsj'h = Pattern.rewrite_term thy [(f,h)] [] rhsj'
 	val compat = get_compat_thm thy compat_store clausei clausej
-	val Ghsj' = map (fn {Gh', ...} => Gh') RCsj
+	val Ghsj' = map (fn RCInfo {Gh', ...} => Gh') RCsj
 
 	val y_eq_rhsj'h = assume (cterm_of thy (Trueprop (mk_eq (y, rhsj'h))))
 	val lhsi_eq_lhsj' = assume (cterm_of thy (Trueprop (mk_eq (lhsi, lhsj')))) (* lhs_i = lhs_j' |-- lhs_i = lhs_j'	*)
@@ -286,17 +286,17 @@
 
 
 
-fun mk_uniqueness_case thy (names:naming_context) ihyp ih_intro G_cases compat_store clauses rep_lemmas (clausei:clause_info) =
+fun mk_uniqueness_case thy names ihyp ih_intro G_cases compat_store clauses rep_lemmas clausei =
     let
-	val {x, y, G, fvar, f, ranT, ...} = names
-	val {lhs, rhs, qs, cqs, ags, case_hyp, lGI, RCs, ...} = clausei
+	val Names {x, y, G, fvar, f, ranT, ...} = names
+	val ClauseInfo {lhs, rhs, qs, cqs, ags, case_hyp, lGI, RCs, ...} = clausei
 
 	val ih_intro_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ih_intro
 
-	fun prep_RC ({lRIq,RIvs, ...} : rec_call_info) = lRIq
-							     |> fold (forall_elim o cterm_of thy o Free) RIvs
-							     |> (fn it => it RS ih_intro_case)
-							     |> fold_rev (forall_intr o cterm_of thy o Free) RIvs
+	fun prep_RC (RCInfo {lRIq,RIvs, ...}) = lRIq
+						    |> fold (forall_elim o cterm_of thy o Free) RIvs
+						    |> (fn it => it RS ih_intro_case)
+						    |> fold_rev (forall_intr o cterm_of thy o Free) RIvs
 
 	val existence = lGI |> instantiate ([], [(cterm_of thy (free_to_var fvar), cterm_of thy f)])
 			    |> fold (curry op COMP o prep_RC) RCs 
@@ -340,10 +340,10 @@
 
 
 (* Does this work with Guards??? *)
-fun mk_domain_intro thy (names:naming_context) R_cases clause =
+fun mk_domain_intro thy names R_cases clause =
     let
-	val {z, R, acc_R, ...} = names
-	val {qs, gs, lhs, rhs, ...} = clause
+	val Names {z, R, acc_R, ...} = names
+	val ClauseInfo {qs, gs, lhs, rhs, ...} = clause
 
 	val z_lhs = cterm_of thy (HOLogic.mk_prod (z,lhs))
 	val z_acc = cterm_of thy (HOLogic.mk_mem (z,acc_R))
@@ -368,10 +368,10 @@
 
 
 
-fun mk_nest_term_case thy (names:naming_context) R' ihyp clause =
+fun mk_nest_term_case thy names R' ihyp clause =
     let
-	val {x, z, ...} = names
-	val {qs,cqs,ags,lhs,rhs,tree,case_hyp,...} = clause
+	val Names {x, z, ...} = names
+	val ClauseInfo {qs,cqs,ags,lhs,rhs,tree,case_hyp,...} = clause
 
 	val ih_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ihyp
 
@@ -421,9 +421,9 @@
     end
 
 
-fun mk_nest_term_rule thy (names:naming_context) clauses =
+fun mk_nest_term_rule thy names clauses =
     let
-	val { R, acc_R, domT, x, z, ... } = names
+	val Names { R, acc_R, domT, x, z, ... } = names
 
 	val R_elim = hd (#elims (snd (the (InductivePackage.get_inductive thy (fst (dest_Const R))))))
 
@@ -469,8 +469,8 @@
 
 fun mk_partial_rules thy congs data complete_thm compat_thms =
     let
-	val {names, clauses, complete, compat, ...} = data
-	val {G, R, acc_R, domT, ranT, f, f_def, x, z, fvarname, ...}:naming_context = names
+	val Prep {names, clauses, complete, compat, ...} = data
+	val Names {G, R, acc_R, domT, ranT, f, f_def, x, z, fvarname, ...}:naming_context = names
 
 (*	val _ = Output.debug "closing derivation: completeness"
 	val _ = Output.debug (Proofterm.size_of_proof (proof_of complete_thm))
@@ -541,7 +541,7 @@
 	val _ = Output.debug "Proving domain introduction rules"
 	val dom_intros = map (mk_domain_intro thy names R_cases) clauses
     in 
-	{f=f, G=G, R=R, compatibility=compat_thms, completeness=complete_thm, 
+	FundefResult {f=f, G=G, R=R, compatibility=compat_thms, completeness=complete_thm, 
 	 psimps=psimps, subset_pinduct=subset_pinduct, simple_pinduct=simple_pinduct, total_intro=total_intro,
 	 dom_intros=dom_intros}
     end
@@ -566,9 +566,9 @@
 
 fun mk_partial_rules_curried thy congs NONE data complete_thm compat_thms =
     mk_partial_rules thy congs data complete_thm compat_thms 
-  | mk_partial_rules_curried thy congs (SOME {curry_ss, argTs}) data complete_thm compat_thms =
+  | mk_partial_rules_curried thy congs (SOME (Curry {curry_ss, argTs})) data complete_thm compat_thms =
     let
-	val {f, G, R, compatibility, completeness, psimps, subset_pinduct,simple_pinduct,total_intro,dom_intros} =
+	val FundefResult {f, G, R, compatibility, completeness, psimps, subset_pinduct,simple_pinduct,total_intro,dom_intros} =
 	    mk_partial_rules thy congs data complete_thm compat_thms 
 	val cpsimps = map (simplify curry_ss) psimps
 	val cpinduct = full_simplify curry_ss simple_pinduct
@@ -576,7 +576,7 @@
 	val cdom_intros = map (full_simplify curry_ss) dom_intros
 	val ctotal_intro = full_simplify curry_ss total_intro
     in
-	{f=f, G=G, R=R, compatibility=compat_thms, completeness=complete_thm, 
+	FundefResult {f=f, G=G, R=R, compatibility=compat_thms, completeness=complete_thm, 
 	 psimps=cpsimps, subset_pinduct=subset_pinduct, simple_pinduct=cpinduct, total_intro=ctotal_intro, dom_intros=cdom_intros}
     end
 
diff -r a669c98b9c24 -r c5fa77b03442 src/HOL/Tools/function_package/termination.ML
--- a/src/HOL/Tools/function_package/termination.ML	Fri May 05 22:11:19 2006 +0200
+++ b/src/HOL/Tools/function_package/termination.ML	Sun May 07 00:00:13 2006 +0200
@@ -20,9 +20,9 @@
 open FundefCommon
 open FundefAbbrev
 
-fun mk_total_termination_goal (data: fundef_result) =
+fun mk_total_termination_goal data =
     let
-	val {R, f, ... } = data
+	val FundefResult {R, f, ... } = data
 
 	val domT = domain_type (fastype_of f)
 	val x = Free ("x", domT)
@@ -30,9 +30,9 @@
 	Trueprop (mk_mem (x, Const (acc_const_name, fastype_of R --> HOLogic.mk_setT domT) $ R))
     end
 
-fun mk_partial_termination_goal thy (data: fundef_result) dom =
+fun mk_partial_termination_goal thy data dom =
     let
-	val {R, f, ... } = data
+	val FundefResult {R, f, ... } = data
 
 	val domT = domain_type (fastype_of f)
 	val D = Sign.simple_read_term thy (Type.varifyT (HOLogic.mk_setT domT)) dom
diff -r a669c98b9c24 -r c5fa77b03442 src/HOL/ex/Fundefs.thy
--- a/src/HOL/ex/Fundefs.thy	Fri May 05 22:11:19 2006 +0200
+++ b/src/HOL/ex/Fundefs.thy	Sun May 07 00:00:13 2006 +0200
@@ -58,7 +58,7 @@
 by pat_completeness auto
 
 lemma nz_is_zero: (* A lemma we need to prove termination *)
-  assumes trm: "x \<in> nz.dom"
+  assumes trm: "x \<in> nz_dom"
   shows "nz x = 0"
 using trm
 by induct auto