--- a/src/HOL/Tools/Function/function_common.ML Sun Nov 01 20:55:39 2009 +0100
+++ b/src/HOL/Tools/Function/function_common.ML Sun Nov 01 20:59:34 2009 +0100
@@ -92,9 +92,7 @@
structure FunctionData = GenericDataFun
(
type T = (term * function_context_data) Item_Net.T;
- val empty = Item_Net.init
- (op aconv o pairself fst : (term * function_context_data) * (term * function_context_data) -> bool)
- fst;
+ val empty : T = Item_Net.init (op aconv o pairself fst) (single o fst);
val copy = I;
val extend = I;
fun merge _ (tab1, tab2) = Item_Net.merge (tab1, tab2)
@@ -138,7 +136,7 @@
val all_function_data = Item_Net.content o get_function
fun add_function_data (data as FunctionCtxData {fs, termination, ...}) =
- FunctionData.map (fold (fn f => Item_Net.insert (f, data)) fs)
+ FunctionData.map (fold (fn f => Item_Net.update (f, data)) fs)
#> store_termination_rule termination
--- a/src/Pure/Isar/calculation.ML Sun Nov 01 20:55:39 2009 +0100
+++ b/src/Pure/Isar/calculation.ML Sun Nov 01 20:59:34 2009 +0100
@@ -66,8 +66,8 @@
(* add/del rules *)
-val trans_add = Thm.declaration_attribute (CalculationData.map o apfst o apfst o Item_Net.insert);
-val trans_del = Thm.declaration_attribute (CalculationData.map o apfst o apfst o Item_Net.delete);
+val trans_add = Thm.declaration_attribute (CalculationData.map o apfst o apfst o Item_Net.update);
+val trans_del = Thm.declaration_attribute (CalculationData.map o apfst o apfst o Item_Net.remove);
val sym_add =
Thm.declaration_attribute (CalculationData.map o apfst o apsnd o Thm.add_thm)
@@ -131,7 +131,8 @@
fun combine ths =
(case opt_rules of SOME rules => rules
| NONE =>
- (case ths of [] => Item_Net.content (#1 (get_rules state))
+ (case ths of
+ [] => Item_Net.content (#1 (get_rules state))
| th :: _ => Item_Net.retrieve (#1 (get_rules state)) (strip_assums_concl th)))
|> Seq.of_list |> Seq.maps (Drule.multi_resolve ths)
|> Seq.filter (not o projection ths);
--- a/src/Pure/consts.ML Sun Nov 01 20:55:39 2009 +0100
+++ b/src/Pure/consts.ML Sun Nov 01 20:59:34 2009 +0100
@@ -71,10 +71,10 @@
(* reverted abbrevs *)
val empty_abbrevs =
- Item_Net.init (fn ((t, u), (t', u')) => t aconv t' andalso u aconv u') #1;
+ Item_Net.init (fn ((t, u), (t', u')) => t aconv t' andalso u aconv u') (single o #1);
-fun insert_abbrevs mode abbrs =
- Symtab.map_default (mode, empty_abbrevs) (Item_Net.insert abbrs);
+fun update_abbrevs mode abbrs =
+ Symtab.map_default (mode, empty_abbrevs) (Item_Net.update abbrs);
fun retrieve_abbrevs (Consts {rev_abbrevs, ...}) modes =
let val nets = map_filter (Symtab.lookup rev_abbrevs) modes
@@ -290,7 +290,7 @@
val (_, decls') = decls
|> Name_Space.define true naming (b, (decl, SOME abbr));
val rev_abbrevs' = rev_abbrevs
- |> insert_abbrevs mode (rev_abbrev lhs rhs);
+ |> update_abbrevs mode (rev_abbrev lhs rhs);
in (decls', constraints, rev_abbrevs') end)
|> pair (lhs, rhs)
end;
@@ -299,7 +299,7 @@
let
val (T, rhs) = the_abbreviation consts c;
val rev_abbrevs' = rev_abbrevs
- |> insert_abbrevs mode (rev_abbrev (Const (c, T)) rhs);
+ |> update_abbrevs mode (rev_abbrev (Const (c, T)) rhs);
in (decls, constraints, rev_abbrevs') end);
end;
--- a/src/Pure/more_thm.ML Sun Nov 01 20:55:39 2009 +0100
+++ b/src/Pure/more_thm.ML Sun Nov 01 20:59:34 2009 +0100
@@ -246,8 +246,8 @@
val del_thm = remove eq_thm_prop;
val merge_thms = merge eq_thm_prop;
-val intro_rules = Item_Net.init eq_thm_prop Thm.concl_of;
-val elim_rules = Item_Net.init eq_thm_prop Thm.major_prem_of;
+val intro_rules = Item_Net.init eq_thm_prop (single o Thm.concl_of);
+val elim_rules = Item_Net.init eq_thm_prop (single o Thm.major_prem_of);
--- a/src/Tools/induct.ML Sun Nov 01 20:55:39 2009 +0100
+++ b/src/Tools/induct.ML Sun Nov 01 20:59:34 2009 +0100
@@ -113,9 +113,10 @@
type rules = (string * thm) Item_Net.T;
-val init_rules =
- Item_Net.init (fn ((s1: string, th1), (s2, th2)) => s1 = s2 andalso
- Thm.eq_thm_prop (th1, th2));
+fun init_rules index : rules =
+ Item_Net.init
+ (fn ((s1, th1), (s2, th2)) => s1 = s2 andalso Thm.eq_thm_prop (th1, th2))
+ (single o index);
fun filter_rules (rs: rules) th =
filter (fn (_, th') => Thm.eq_thm_prop (th, th')) (Item_Net.content rs);
@@ -203,18 +204,18 @@
let val (x, thm) = g arg in (InductData.map (f (name, thm)) x, thm) end;
fun del_att which = Thm.declaration_attribute (fn th => InductData.map (which (pairself (fn rs =>
- fold Item_Net.delete (filter_rules rs th) rs))));
+ fold Item_Net.remove (filter_rules rs th) rs))));
fun map1 f (x, y, z) = (f x, y, z);
fun map2 f (x, y, z) = (x, f y, z);
fun map3 f (x, y, z) = (x, y, f z);
-fun add_casesT rule x = map1 (apfst (Item_Net.insert rule)) x;
-fun add_casesP rule x = map1 (apsnd (Item_Net.insert rule)) x;
-fun add_inductT rule x = map2 (apfst (Item_Net.insert rule)) x;
-fun add_inductP rule x = map2 (apsnd (Item_Net.insert rule)) x;
-fun add_coinductT rule x = map3 (apfst (Item_Net.insert rule)) x;
-fun add_coinductP rule x = map3 (apsnd (Item_Net.insert rule)) x;
+fun add_casesT rule x = map1 (apfst (Item_Net.update rule)) x;
+fun add_casesP rule x = map1 (apsnd (Item_Net.update rule)) x;
+fun add_inductT rule x = map2 (apfst (Item_Net.update rule)) x;
+fun add_inductP rule x = map2 (apsnd (Item_Net.update rule)) x;
+fun add_coinductT rule x = map3 (apfst (Item_Net.update rule)) x;
+fun add_coinductP rule x = map3 (apsnd (Item_Net.update rule)) x;
val consumes0 = Rule_Cases.consumes_default 0;
val consumes1 = Rule_Cases.consumes_default 1;