tuned names (to make them independent from temporary naming convention used in characteristic theorems)
authorblanchet
Sat, 26 Oct 2013 12:57:17 +0200
changeset 54207 9296ebf40db0
parent 54206 1c26d55b8d73
child 54208 513e91175170
tuned names (to make them independent from temporary naming convention used in characteristic theorems)
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;