--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML Wed Sep 25 17:11:17 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML Wed Sep 25 18:00:53 2013 +0200
@@ -255,7 +255,7 @@
fun check_no_call t = if has_call t then unexpected_corec_call ctxt t else ();
- fun massage_abs bound_Ts (Abs (s, T, t)) = massage_abs (T :: bound_Ts) t
+ fun massage_abs bound_Ts (Abs (s, T, t)) = Abs (s, T, massage_abs (T :: bound_Ts) t)
| massage_abs bound_Ts t = massage_rec bound_Ts t
and massage_rec bound_Ts t =
let val typof = curry fastype_of1 bound_Ts in
@@ -269,7 +269,7 @@
| (Const (c, _), args as _ :: _) =>
let val n = num_binder_types (Sign.the_const_type thy c) - 1 in
if n < length args then
- (case fastype_of1 (bound_Ts, nth args n) of
+ (case typof (nth args n) of
Type (s, Ts) =>
if case_of ctxt s = SOME c then
let
@@ -278,7 +278,7 @@
val casex' = Const (c, map typof branches' ---> map typof obj_leftovers --->
typof t);
in
- betapplys (casex', branches' @ tap (List.app check_no_call) obj_leftovers)
+ Term.list_comb (casex', branches' @ tap (List.app check_no_call) obj_leftovers)
end
else
massage_leaf bound_Ts t