diff -r dce2168b0ea4 -r c62720b20e9a src/HOL/Tools/function_package/fundef_common.ML
--- a/src/HOL/Tools/function_package/fundef_common.ML	Mon Jun 05 21:54:26 2006 +0200
+++ b/src/HOL/Tools/function_package/fundef_common.ML	Tue Jun 06 08:21:14 2006 +0200
@@ -40,17 +40,17 @@
 
 
 datatype rec_call_info = 
-  RCInfo 
-  of {
-  RI: thm, 
-  RIvs: (string * typ) list,
-  lRI: thm, 
-  lRIq: thm, 
-  Gh: thm, 
-  Gh': thm,
-  GmAs: term list,
-  rcarg: term
-} 
+  RCInfo of
+  {
+   RI: thm, 
+   RIvs: (string * typ) list,
+   lRI: thm, 
+   lRIq: thm, 
+   Gh: thm, 
+   Gh': thm,
+   GmAs: term list,
+   rcarg: term
+  } 
      
 datatype clause_info =
   ClauseInfo of 
@@ -80,10 +80,6 @@
       case_hyp: thm
      }
 
-
-datatype curry_info =
-  Curry of { argTs: typ list, curry_ss: simpset }
-
 type inj_proj = ((term -> term) * (term -> term))
 
 type qgar = (string * typ) list * term list * term list * term