# HG changeset patch
# User bulwahn
# Date 1267433264 -3600
# Node ID cafb74a131da7a78ddfd23d9377c91bd48d36c8b
# Parent  1ea89d2a1bd4cceb71406a4ae1d61cb51a34a6ea
made smlnj happy

diff -r 1ea89d2a1bd4 -r cafb74a131da src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Sun Feb 28 23:51:31 2010 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Mon Mar 01 09:47:44 2010 +0100
@@ -897,7 +897,7 @@
 
 (** mode analysis **)
 
-(* options for mode analysis  are: #use_random, #reorder_premises *)
+type mode_analysis_options = {use_random : bool, reorder_premises : bool, infer_pos_and_neg_modes : bool}
 
 fun is_constrt thy =
   let
@@ -1178,7 +1178,7 @@
   tracing ("modes: " ^ (commas (map (fn (s, ms) => s ^ ": " ^
     commas (map (fn (m, r) => string_of_mode m ^ (if r then " random " else " not ")) ms)) modes)))
 
-fun select_mode_prem mode_analysis_options thy pol (modes, (pos_modes, neg_modes)) vs ps =
+fun select_mode_prem (mode_analysis_options : mode_analysis_options) thy pol (modes, (pos_modes, neg_modes)) vs ps =
   let
     fun choose_mode_of_prem (Prem t) = partial_hd
         (sort (deriv_ord2 thy modes t) (all_derivations_of thy pos_modes vs t))
@@ -1194,7 +1194,7 @@
       SOME (hd ps, choose_mode_of_prem (hd ps))
   end
 
-fun check_mode_clause' mode_analysis_options thy param_vs (modes :
+fun check_mode_clause' (mode_analysis_options : mode_analysis_options) thy param_vs (modes :
   (string * ((bool * mode) * bool) list) list) ((pol, mode) : bool * mode) (ts, ps) =
   let
     val vTs = distinct (op =) (fold Term.add_frees (map term_of_prem ps) (fold Term.add_frees ts []))
diff -r 1ea89d2a1bd4 -r cafb74a131da src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Sun Feb 28 23:51:31 2010 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Mon Mar 01 09:47:44 2010 +0100
@@ -22,7 +22,8 @@
 structure Fun_Pred = Theory_Data
 (
   type T = (term * term) Item_Net.T;
-  val empty = Item_Net.init (op aconv o pairself fst) (single o fst);
+  val empty = Item_Net.init ((op aconv o pairself fst) : (term * term) * (term * term) -> bool)
+    (single o fst);
   val extend = I;
   val merge = Item_Net.merge;
 )
diff -r 1ea89d2a1bd4 -r cafb74a131da src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Sun Feb 28 23:51:31 2010 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Mon Mar 01 09:47:44 2010 +0100
@@ -23,7 +23,7 @@
 fun datatype_names_of_case_name thy case_name =
   map (#1 o #2) (#descr (the (Datatype_Data.info_of_case thy case_name)))
 
-fun make_case_rewrites new_type_names descr sorts thy =
+fun make_case_distribs new_type_names descr sorts thy =
   let
     val case_combs = Datatype_Prop.make_case_combs new_type_names descr sorts thy "f";
     fun make comb =
@@ -58,7 +58,7 @@
     val typ_names = the_default [Tcon] (#alt_names info)
   in
     map (Drule.export_without_context o Skip_Proof.make_thm thy o HOLogic.mk_Trueprop)
-      (make_case_rewrites typ_names [descr] sorts thy)
+      (make_case_distribs typ_names [descr] sorts thy)
   end
 
 fun instantiated_case_rewrites thy Tcon =