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