# HG changeset patch
# User wenzelm
# Date 1003171008 -7200
# Node ID b66b198ee29af9e019aebe897e354c3e9fb381f8
# Parent  aee100a086b10471d9e9dccc3bcc53ce823c3298
tuned NetRules;

diff -r aee100a086b1 -r b66b198ee29a src/Pure/Isar/calculation.ML
--- a/src/Pure/Isar/calculation.ML	Mon Oct 15 20:36:04 2001 +0200
+++ b/src/Pure/Isar/calculation.ML	Mon Oct 15 20:36:48 2001 +0200
@@ -36,7 +36,7 @@
   val name = "Isar/calculation";
   type T = thm NetRules.T
 
-  val empty = NetRules.init_elim;
+  val empty = NetRules.elim;
   val copy = I;
   val prep_ext = I;
   val merge = NetRules.merge;
@@ -131,7 +131,7 @@
       (case opt_rules of Some rules => rules
       | None =>
           (case ths of [] => NetRules.rules (get_local_rules state)
-          | th :: _ => NetRules.may_unify (get_local_rules state) (strip_assums_concl th)))
+          | th :: _ => NetRules.retrieve (get_local_rules state) (strip_assums_concl th)))
       |> Seq.of_list |> Seq.map (Method.multi_resolve ths) |> Seq.flat
       |> Seq.filter (not o projection ths);
 
diff -r aee100a086b1 -r b66b198ee29a src/Pure/Isar/induct_attrib.ML
--- a/src/Pure/Isar/induct_attrib.ML	Mon Oct 15 20:36:04 2001 +0200
+++ b/src/Pure/Isar/induct_attrib.ML	Mon Oct 15 20:36:48 2001 +0200
@@ -84,7 +84,7 @@
 type rules = (string * thm) NetRules.T;
 
 val init_rules = NetRules.init (fn ((s1: string, th1), (s2, th2)) => s1 = s2
-  andalso Thm.eq_thm (th1, th2));
+  andalso Thm.eq_thm (th1, th2)) (K 0);
 
 fun lookup_rule (rs: rules) name = Library.assoc (NetRules.rules rs, name);
 
@@ -153,7 +153,7 @@
 
 
 fun find_rules which how ctxt x =
-  map snd (NetRules.may_unify (which (LocalInduct.get ctxt)) (how x));
+  map snd (NetRules.retrieve (which (LocalInduct.get ctxt)) (how x));
 
 val find_casesT = find_rules (#1 o #1) encode_type;
 val find_casesS = find_rules (#2 o #1) Thm.concl_of;