# HG changeset patch
# User blanchet
# Date 1390319794 -3600
# Node ID 697b41533e1a25965851de5158dabf313749030d
# Parent  79c92e2dc35934b5a6ed1bba3bf58ea18ce54895
made SML/NJ happier

diff -r 79c92e2dc359 -r 697b41533e1a src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Tue Jan 21 14:52:23 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Tue Jan 21 16:56:34 2014 +0100
@@ -876,7 +876,8 @@
       end
   end;
 
-fun find_corec_calls ctxt has_call basic_ctr_specs ({ctr, sel, rhs_term, ...} : coeqn_data_sel) =
+fun find_corec_calls ctxt has_call (basic_ctr_specs : basic_corec_ctr_spec list)
+    ({ctr, sel, rhs_term, ...} : coeqn_data_sel) =
   let
     val sel_no = find_first (curry (op =) ctr o #ctr) basic_ctr_specs
       |> find_index (curry (op =) sel) o #sels o the;
@@ -1162,7 +1163,8 @@
                 |> single
             end;
 
-        fun prove_code exhaustive disc_eqns sel_eqns nchotomys ctr_alist ctr_specs =
+        fun prove_code exhaustive (disc_eqns : coeqn_data_disc list)
+            (sel_eqns : coeqn_data_sel list) nchotomys ctr_alist ctr_specs =
           let
             val fun_data_opt =
               (find_first (member (op =) (map #ctr ctr_specs) o #ctr) disc_eqns,
@@ -1190,7 +1192,7 @@
                     in SOME (false, rhs, raw_rhs, ctr_thms) end
                   | NONE =>
                     let
-                      fun prove_code_ctr {ctr, sels, ...} =
+                      fun prove_code_ctr ({ctr, sels, ...} : corec_ctr_spec) =
                         if not (exists (curry (op =) ctr o fst) ctr_alist) then NONE else
                           let
                             val prems = find_first (curry (op =) ctr o #ctr) disc_eqns