# HG changeset patch
# User blanchet
# Date 1380556424 -7200
# Node ID 65fc58793ed57b22a31ad8c7e7a1655c69e0e4e7
# Parent  9cfff7f61d0d015e7fb049bc6474c6f4912ceb1b
made SML/NJ happier

diff -r 9cfff7f61d0d -r 65fc58793ed5 src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Mon Sep 30 17:47:50 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Mon Sep 30 17:53:44 2013 +0200
@@ -189,7 +189,7 @@
       primrec_error_eqn "recursive call not directly applied to constructor argument" t)
   end;
 
-fun build_rec_arg lthy funs_data has_call ctr_spec maybe_eqn_data =
+fun build_rec_arg lthy (funs_data : eqn_data list) has_call ctr_spec maybe_eqn_data =
   if is_none maybe_eqn_data then undef_const else
     let
       val eqn_data = the maybe_eqn_data;
@@ -243,7 +243,7 @@
       |> fold_rev lambda abstractions
     end;
 
-fun build_defs lthy bs mxs funs_data rec_specs has_call =
+fun build_defs lthy bs mxs (funs_data : eqn_data list) rec_specs has_call =
   let
     val n_funs = length funs_data;
 
@@ -275,7 +275,7 @@
     |> map3 (fn b => fn mx => fn t => ((b, mx), ((Binding.map_name Thm.def_name b, []), t))) bs mxs
   end;
 
-fun find_rec_calls has_call eqn_data =
+fun find_rec_calls has_call (eqn_data : eqn_data) =
   let
     fun find (Abs (_, _, b)) ctr_arg = find b ctr_arg
       | find (t as _ $ _) ctr_arg =
@@ -329,8 +329,8 @@
 
     val defs = build_defs lthy' bs mxs funs_data rec_specs has_call;
 
-    fun prove def_thms' {ctr_specs, nested_map_idents, nested_map_comps, ...} induct_thm fun_data
-        lthy =
+    fun prove def_thms' ({nested_map_idents, nested_map_comps, ctr_specs, ...} : rec_spec)
+        induct_thm fun_data lthy =
       let
         val fun_name = #fun_name (hd fun_data);
         val def_thms = map (snd o snd) def_thms';
@@ -397,6 +397,7 @@
   auto_gen: bool,
   user_eqn: term
 };
+
 type co_eqn_data_sel = {
   fun_name: string,
   fun_T: typ,
@@ -406,6 +407,7 @@
   rhs_term: term,
   user_eqn: term
 };
+
 datatype co_eqn_data =
   Disc of co_eqn_data_disc |
   Sel of co_eqn_data_sel;