# HG changeset patch
# User blanchet
# Date 1380573403 -7200
# Node ID c4343c31f86d43582757cbeb19603a67098e433c
# Parent  01c8f9d3b0843787b55b9c285596b1c2d4c7443d
made SML/NJ happy

diff -r 01c8f9d3b084 -r c4343c31f86d src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Mon Sep 30 18:08:35 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Mon Sep 30 22:36:43 2013 +0200
@@ -189,7 +189,8 @@
       primrec_error_eqn "recursive call not directly applied to constructor argument" t)
   end;
 
-fun build_rec_arg lthy (funs_data : eqn_data list list) has_call ctr_spec maybe_eqn_data =
+fun build_rec_arg lthy (funs_data : eqn_data list list) has_call (ctr_spec : rec_ctr_spec)
+    (maybe_eqn_data : eqn_data option) =
   if is_none maybe_eqn_data then undef_const else
     let
       val eqn_data = the maybe_eqn_data;
@@ -243,7 +244,7 @@
       |> fold_rev lambda abstractions
     end;
 
-fun build_defs lthy bs mxs (funs_data : eqn_data list list) rec_specs has_call =
+fun build_defs lthy bs mxs (funs_data : eqn_data list list) (rec_specs : rec_spec list) has_call =
   let
     val n_funs = length funs_data;
 
@@ -330,7 +331,7 @@
     val defs = build_defs lthy' bs mxs funs_data rec_specs has_call;
 
     fun prove def_thms' ({nested_map_idents, nested_map_comps, ctr_specs, ...} : rec_spec)
-        induct_thm fun_data lthy =
+        induct_thm (fun_data : eqn_data list) lthy =
       let
         val fun_name = #fun_name (hd fun_data);
         val def_thms = map (snd o snd) def_thms';
diff -r 01c8f9d3b084 -r c4343c31f86d src/HOL/BNF/Tools/bnf_lfp_compat.ML
--- a/src/HOL/BNF/Tools/bnf_lfp_compat.ML	Mon Sep 30 18:08:35 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp_compat.ML	Mon Sep 30 22:36:43 2013 +0200
@@ -14,6 +14,7 @@
 struct
 
 open BNF_Util
+open BNF_Ctr_Sugar
 open BNF_FP_Util
 open BNF_FP_Def_Sugar
 open BNF_FP_N2M_Sugar
@@ -106,14 +107,14 @@
 
     fun mk_ctr_descr (Const (s, T)) =
       (s, map mk_dtyp (binder_types (Type.legacy_freeze_type T)));
-    fun mk_typ_descr index (Type (T_name, Ts)) {ctrs, ...} =
+    fun mk_typ_descr index (Type (T_name, Ts)) ({ctrs, ...} : ctr_sugar) =
       (index, (T_name, map mk_dtyp Ts, map mk_ctr_descr ctrs));
 
     val descr = map3 mk_typ_descr (0 upto nn - 1) frozen_Ts ctr_sugars;
     val recs = map (fst o dest_Const o co_rec_of) co_iterss;
     val rec_thms = flat (map co_rec_of iter_thmsss);
 
-    fun mk_info {T = Type (T_name0, _), index, ...} =
+    fun mk_info ({T = Type (T_name0, _), index, ...} : fp_sugar) =
       let
         val {casex, exhaust, nchotomy, injects, distincts, case_thms, case_cong, weak_case_cong,
           split, split_asm, ...} = nth ctr_sugars index;