# HG changeset patch # User wenzelm # Date 1121263641 -7200 # Node ID 90eff1b524282c144ab19ee172f100825e9930d1 # Parent 978dcf30c3dd7e6c76ce38c804de1807bdb3f10c improved Net interface; diff -r 978dcf30c3dd -r 90eff1b52428 src/FOLP/simp.ML --- a/src/FOLP/simp.ML Wed Jul 13 16:07:18 2005 +0200 +++ b/src/FOLP/simp.ML Wed Jul 13 16:07:21 2005 +0200 @@ -68,7 +68,7 @@ (*insert a thm in a discrimination net by its lhs*) fun lhs_insert_thm (th,net) = - Net.insert_term((lhs_of (concl_of th), (false,th)), net, eq_brl) + Net.insert_term eq_brl (lhs_of (concl_of th), (false,th)) net handle Net.INSERT => net; (*match subgoal i against possible theorems in the net. @@ -247,7 +247,7 @@ (*insert a thm in a thm net*) fun insert_thm_warn (th,net) = - Net.insert_term((concl_of th, th), net, Drule.eq_thm_prop) + Net.insert_term Drule.eq_thm_prop (concl_of th, th) net handle Net.INSERT => (writeln"\nDuplicate rewrite or congruence rule:"; print_thm th; net); @@ -273,7 +273,7 @@ (*delete a thm from a thm net*) fun delete_thm_warn (th,net) = - Net.delete_term((concl_of th, th), net, Drule.eq_thm_prop) + Net.delete_term Drule.eq_thm_prop (concl_of th, th) net handle Net.DELETE => (writeln"\nNo such rewrite or congruence rule:"; print_thm th; net); diff -r 978dcf30c3dd -r 90eff1b52428 src/HOL/Tools/res_axioms.ML --- a/src/HOL/Tools/res_axioms.ML Wed Jul 13 16:07:18 2005 +0200 +++ b/src/HOL/Tools/res_axioms.ML Wed Jul 13 16:07:21 2005 +0200 @@ -250,7 +250,7 @@ |> ObjectLogic.atomize_thm |> make_nnf; (*The cache prevents repeated clausification of a theorem, - and also repeated declaration of Skolem functions*) + and also repeated declaration of Skolem functions*) (* FIXME better use Termtab!? *) val clause_cache = ref (Symtab.empty : (thm * thm list) Symtab.table) (*Declare Skolem functions for a theorem, supplied in nnf and with its name*) @@ -366,10 +366,8 @@ end; fun simpset_rules_of_thy thy = - let val rules = #rules(fst (rep_ss (simpset_of thy))) - in - map (fn (_,r) => (#name r, #thm r)) (Net.dest rules) - end; + let val rules = #rules (fst (rep_ss (simpset_of thy))) + in map (fn r => (#name r, #thm r)) (Net.entries rules) end; (**** Translate a set of classical/simplifier rules into CNF (still as type "thm") ****) diff -r 978dcf30c3dd -r 90eff1b52428 src/Pure/Isar/net_rules.ML --- a/src/Pure/Isar/net_rules.ML Wed Jul 13 16:07:18 2005 +0200 +++ b/src/Pure/Isar/net_rules.ML Wed Jul 13 16:07:21 2005 +0200 @@ -47,7 +47,7 @@ fun add rule (Rules {eq, index, rules, next, net}) = mk_rules eq index (rule :: rules) (next - 1) - (Net.insert_term ((index rule, (next, rule)), net, K false)); + (Net.insert_term (K false) (index rule, (next, rule)) net); fun merge (Rules {eq, index, rules = rules1, ...}, Rules {rules = rules2, ...}) = let val rules = Library.gen_merge_lists' eq rules1 rules2 @@ -56,7 +56,7 @@ fun delete rule (rs as Rules {eq, index, rules, next, net}) = if not (Library.gen_mem eq (rule, rules)) then rs else mk_rules eq index (Library.gen_rem eq (rules, rule)) next - (Net.delete_term ((index rule, (0, rule)), net, eq o pairself #2)); + (Net.delete_term (eq o pairself #2) (index rule, (0, rule)) net); fun insert rule rs = add rule (delete rule rs); (*ensure that new rule gets precedence*) diff -r 978dcf30c3dd -r 90eff1b52428 src/Pure/Proof/extraction.ML --- a/src/Pure/Proof/extraction.ML Wed Jul 13 16:07:18 2005 +0200 +++ b/src/Pure/Proof/extraction.ML Wed Jul 13 16:07:21 2005 +0200 @@ -79,8 +79,8 @@ val empty_rules : rules = {next = 0, rs = [], net = Net.empty}; fun add_rule (r as (_, (lhs, _)), {next, rs, net} : rules) = - {next = next - 1, rs = r :: rs, net = Net.insert_term - ((Pattern.eta_contract lhs, (next, r)), net, K false)}; + {next = next - 1, rs = r :: rs, net = Net.insert_term (K false) + (Pattern.eta_contract lhs, (next, r)) net}; fun merge_rules ({next, rs = rs1, net} : rules) ({next = next2, rs = rs2, ...} : rules) = @@ -316,7 +316,7 @@ ExtractionData.get thy; val procs = List.concat (map (fst o snd) types); val rtypes = map fst types; - val eqns = Net.merge (#net realizes_eqns, #net typeof_eqns, K false); + val eqns = Net.merge (K false) (#net realizes_eqns, #net typeof_eqns); val thy' = add_syntax thy; val rd = ProofSyntax.read_proof thy' false in fn (thm, (vs, s1, s2)) => @@ -351,7 +351,7 @@ val {realizes_eqns, typeof_eqns, defs, types, ...} = ExtractionData.get thy'; val procs = List.concat (map (fst o snd) types); - val eqns = Net.merge (#net realizes_eqns, #net typeof_eqns, K false); + val eqns = Net.merge (K false) (#net realizes_eqns, #net typeof_eqns); val prop' = Pattern.rewrite_term (Sign.tsig_of thy') (map (Logic.dest_equals o prop_of) defs) [] prop; in freeze_thaw (condrew thy' eqns @@ -470,7 +470,7 @@ val typroc = typeof_proc (Sign.defaultS thy'); val prep = getOpt (prep, K I) thy' o ProofRewriteRules.elim_defs thy' false defs o Reconstruct.expand_proof thy' (("", NONE) :: map (apsnd SOME) expand); - val rrews = Net.merge (#net realizes_eqns, #net typeof_eqns, K false); + val rrews = Net.merge (K false) (#net realizes_eqns, #net typeof_eqns); fun find_inst prop Ts ts vs = let diff -r 978dcf30c3dd -r 90eff1b52428 src/ZF/Tools/typechk.ML --- a/src/ZF/Tools/typechk.ML Wed Jul 13 16:07:18 2005 +0200 +++ b/src/ZF/Tools/typechk.ML Wed Jul 13 16:07:21 2005 +0200 @@ -58,12 +58,12 @@ cs) else TC{rules = th::rules, - net = Net.insert_term ((concl_of th, th), net, K false)}; + net = Net.insert_term (K false) (concl_of th, th) net}; fun delTC (cs as TC{rules, net}, th) = if mem_thm (th, rules) then - TC{net = Net.delete_term ((concl_of th, th), net, Drule.eq_thm_prop), + TC{net = Net.delete_term Drule.eq_thm_prop (concl_of th, th) net, rules = rem_thm (rules,th)} else (warning ("No such type-checking rule\n" ^ (string_of_thm th)); cs); @@ -113,7 +113,7 @@ fun merge_tc (TC{rules,net}, TC{rules=rules',net=net'}) = TC {rules = gen_union Drule.eq_thm_prop (rules,rules'), - net = Net.merge (net, net', Drule.eq_thm_prop)}; + net = Net.merge Drule.eq_thm_prop (net, net')}; (*print tcsets*) fun print_tc (TC{rules,...}) =