--- 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