--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Wed Sep 05 10:53:51 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Wed Sep 05 11:08:18 2012 +0200
@@ -99,9 +99,14 @@
|> mk_TFrees N
||> the_single o fst o mk_TFrees 1;
- fun freeze_rec (T as Type (s, Ts')) =
- (case find_index (curry (op =) T) Ts of
- ~1 => Type (s, map freeze_rec Ts')
+ fun is_same_rec (T as Type (s, Us)) (Type (s', Us')) =
+ s = s' andalso (Us = Us' orelse error ("Illegal occurrence of recursive type " ^
+ quote (Syntax.string_of_typ fake_lthy T)))
+ | is_same_rec _ _ = false
+
+ fun freeze_rec (T as Type (s, Us)) =
+ (case find_index (is_same_rec T) Ts of
+ ~1 => Type (s, map freeze_rec Us)
| i => nth Bs i)
| freeze_rec T = T;
@@ -210,11 +215,17 @@
fun sugar_lfp lthy =
let
(*###
- val iter_Tss = map ( ) ctr_Tss
+ val fld_iter = @{term True}; (*###*)
+
+ val iter_Tss = map (fn Ts => Ts) (*###*) ctr_Tss;
val iter_Ts = map (fn Ts => Ts ---> C) iter_Tss;
val iter_fs = map2 (fn Free (s, _) => fn T => Free (s, T)) fs iter_Ts
+ val iter_rhs =
+ fold_rev Term.lambda fs (fld_iter $ mk_sum_caseN (uncurry_fs fs xss) $ (unf $ v));
+
+
val uncurried_fs =
map2 (fn f => fn xs =>
HOLogic.tupled_lambda (HOLogic.mk_tuple xs) (Term.list_comb (f, xs))) fs xss;