src/HOL/Tools/function_package/fundef_prep.ML

     end
 
 
 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)
 	val rw_RI_to_h_assum = (mk_mem (mk_prod (zv, xv), R),
 				mk_mem (mk_prod (zv, h $ zv), G))

 			  
 		val Gh_term = Pattern.rewrite_term thy [rw_RI_to_h_assum, rw_f_to_h] [] (prop_of lRIq)
 		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
 
 
 
 

 				    Const ("The", (ranT --> boolT) --> ranT) $
 					  Abs ("y", ranT, mk_relmemT domT ranT (x, Bound 0) G))
 
 	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
 
 
 (* Gs ==> Gs' ==> lhs = lhs' ==> rhs = rhs' *)
 fun mk_compat_impl ((qs, gs, lhs, rhs),(qs', gs', lhs', rhs')) =

 	(map (map dest_Free) vRis, preRis, Ris)
     end
 
 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)
 
 	val rew1 = (mk_mem (mk_prod (z, x), R),

 		  |> fold_rev (curry Logic.mk_implies) gs
     end
 
 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)))
 						|> fold_rev (curry Logic.mk_implies) gs
 						|> fold_rev mk_forall qs

     end
 
 
 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
 	val complete = mk_completeness names glrs
 	val compat = mk_compat_proof_obligations glrs glrs'

  * and comatibility conditions and returns everything.
  *)
 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
 
 	val (G_intro_thms, (thy, _)) = inductive_def G_intros (thy, G)
 	val (R_intro_thmss, (thy, _)) = fold_burrow inductive_def R_intross (thy, R)
 
 	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
 
 
 

 		val ([f_def], thy) = PureThy.add_defs_i false [((fxname ^ "_def", def), [])] thy
 				      
 		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