--- 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 []))
--- 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;
)
--- 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 =