# HG changeset patch
# User blanchet
# Date 1382785037 -7200
# Node ID 9296ebf40db09f3b40c76a577a0dbc87172645b5
# Parent  1c26d55b8d730c9a7295bf250286ada98f35c399
tuned names (to make them independent from temporary naming convention used in characteristic theorems)

diff -r 1c26d55b8d73 -r 9296ebf40db0 src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML
--- 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;