equal
deleted
inserted
replaced
36 |
36 |
37 fun rules (Rules {rules = rs, ...}) = rs; |
37 fun rules (Rules {rules = rs, ...}) = rs; |
38 |
38 |
39 fun retrieve (Rules {rules, net, ...}) tm = |
39 fun retrieve (Rules {rules, net, ...}) tm = |
40 Tactic.untaglist |
40 Tactic.untaglist |
41 ((Library.sort (Int.compare o pairself #1) (Net.unify_term net tm))); |
41 ((Library.sort (int_ord o pairself #1) (Net.unify_term net tm))); |
42 |
42 |
43 |
43 |
44 (* build rules *) |
44 (* build rules *) |
45 |
45 |
46 fun init eq index = mk_rules eq index [] ~1 Net.empty; |
46 fun init eq index = mk_rules eq index [] ~1 Net.empty; |