# HG changeset patch # User wenzelm # Date 1257105574 -3600 # Node ID 674df68d4df0c93e5634d4e95a50a95bf80c305d # Parent f380fbd6e32902eabcde87b71fa0d363462ffd02 adapted Item_Net; tuned; diff -r f380fbd6e329 -r 674df68d4df0 src/HOL/Tools/Function/function_common.ML --- 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 diff -r f380fbd6e329 -r 674df68d4df0 src/Pure/Isar/calculation.ML --- 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); diff -r f380fbd6e329 -r 674df68d4df0 src/Pure/consts.ML --- 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; diff -r f380fbd6e329 -r 674df68d4df0 src/Pure/more_thm.ML --- 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); diff -r f380fbd6e329 -r 674df68d4df0 src/Tools/induct.ML --- 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;