# HG changeset patch
# User blanchet
# Date 1428662681 -7200
# Node ID b0816837ef4b02e4e2e324671df3870e20008d2a
# Parent  3fa68bacfa2ba7b159a55806a11754fc1b766fca
exported function (for symmetry)

diff -r 3fa68bacfa2b -r b0816837ef4b src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML	Fri Apr 10 12:16:58 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML	Fri Apr 10 12:44:41 2015 +0200
@@ -6,7 +6,13 @@
 More recursor sugar.
 *)
 
-structure BNF_LFP_Rec_Sugar_More : sig end =
+signature BNF_LFP_REC_SUGAR_MORE =
+sig
+  val massage_nested_rec_call: Proof.context -> (term -> bool) -> (typ -> typ -> term -> term) ->
+    typ list -> term -> term -> term -> term
+end;
+
+structure BNF_LFP_Rec_Sugar_More : BNF_LFP_REC_SUGAR_MORE =
 struct
 
 open BNF_Util
@@ -71,7 +77,7 @@
 fun unexpected_rec_call ctxt t =
   error ("Unexpected recursive call: " ^ quote (Syntax.string_of_term ctxt t));
 
-fun massage_nested_rec_call ctxt has_call raw_massage_fun bound_Ts y y' =
+fun massage_nested_rec_call ctxt has_call massage_fun bound_Ts y y' =
   let
     fun check_no_call t = if has_call t then unexpected_rec_call ctxt t else ();
 
@@ -91,7 +97,7 @@
       | _ =>
         if has_call t then
           (case try HOLogic.dest_prodT U of
-            SOME (U1, U2) => if U1 = T then raw_massage_fun T U2 t else invalid_map ctxt t
+            SOME (U1, U2) => if U1 = T then massage_fun T U2 t else invalid_map ctxt t
           | NONE => invalid_map ctxt t)
         else
           mk_comp bound_Ts (t, build_map_fst (U, T)));