exported function (for symmetry)
authorblanchet
Fri Apr 10 12:44:41 2015 +0200 (2015-04-10)
changeset 60000b0816837ef4b
parent 59999 3fa68bacfa2b
child 60001 0e1b220ec4c9
exported function (for symmetry)
src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML
     1.1 --- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML	Fri Apr 10 12:16:58 2015 +0200
     1.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML	Fri Apr 10 12:44:41 2015 +0200
     1.3 @@ -6,7 +6,13 @@
     1.4  More recursor sugar.
     1.5  *)
     1.6  
     1.7 -structure BNF_LFP_Rec_Sugar_More : sig end =
     1.8 +signature BNF_LFP_REC_SUGAR_MORE =
     1.9 +sig
    1.10 +  val massage_nested_rec_call: Proof.context -> (term -> bool) -> (typ -> typ -> term -> term) ->
    1.11 +    typ list -> term -> term -> term -> term
    1.12 +end;
    1.13 +
    1.14 +structure BNF_LFP_Rec_Sugar_More : BNF_LFP_REC_SUGAR_MORE =
    1.15  struct
    1.16  
    1.17  open BNF_Util
    1.18 @@ -71,7 +77,7 @@
    1.19  fun unexpected_rec_call ctxt t =
    1.20    error ("Unexpected recursive call: " ^ quote (Syntax.string_of_term ctxt t));
    1.21  
    1.22 -fun massage_nested_rec_call ctxt has_call raw_massage_fun bound_Ts y y' =
    1.23 +fun massage_nested_rec_call ctxt has_call massage_fun bound_Ts y y' =
    1.24    let
    1.25      fun check_no_call t = if has_call t then unexpected_rec_call ctxt t else ();
    1.26  
    1.27 @@ -91,7 +97,7 @@
    1.28        | _ =>
    1.29          if has_call t then
    1.30            (case try HOLogic.dest_prodT U of
    1.31 -            SOME (U1, U2) => if U1 = T then raw_massage_fun T U2 t else invalid_map ctxt t
    1.32 +            SOME (U1, U2) => if U1 = T then massage_fun T U2 t else invalid_map ctxt t
    1.33            | NONE => invalid_map ctxt t)
    1.34          else
    1.35            mk_comp bound_Ts (t, build_map_fst (U, T)));