tuned names (to make them independent from temporary naming convention used in characteristic theorems)
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML Sat Oct 26 12:54:57 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML Sat Oct 26 12:57:17 2013 +0200
@@ -689,16 +689,14 @@
let
val {fun_args, rhs_term, ... } = the maybe_sel_eqn;
val bound_Ts = List.rev (map fastype_of fun_args);
- fun rewrite_q _ t = if has_call t then @{term False} else @{term True};
- fun rewrite_g _ t = if has_call t then undef_const else t;
- fun rewrite_h bound_Ts t =
+ fun rewrite_stop _ t = if has_call t then @{term False} else @{term True};
+ fun rewrite_end _ t = if has_call t then undef_const else t;
+ fun rewrite_cont bound_Ts t =
if has_call t then mk_tuple1 bound_Ts (snd (strip_comb t)) else undef_const;
fun massage f _ = massage_mutual_corec_call lthy has_call f bound_Ts rhs_term
|> abs_tuple fun_args;
in
- (massage rewrite_q,
- massage rewrite_g,
- massage rewrite_h)
+ (massage rewrite_stop, massage rewrite_end, massage rewrite_cont)
end
end;