# HG changeset patch
# User wenzelm
# Date 1007518532 -3600
# Node ID 5177845a34f5dbab02abdd2d5c5f11761f9fd428
# Parent  3402d300f5eff5371b3d805e0d21881abc52bfc8
simplified NetRules;

diff -r 3402d300f5ef -r 5177845a34f5 src/Pure/Isar/induct_attrib.ML
--- a/src/Pure/Isar/induct_attrib.ML	Wed Dec 05 03:15:15 2001 +0100
+++ b/src/Pure/Isar/induct_attrib.ML	Wed Dec 05 03:15:32 2001 +0100
@@ -83,8 +83,8 @@
 
 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)) (K 0);
+val init_rules =
+  NetRules.init (fn ((s1: string, th1), (s2, th2)) => s1 = s2 andalso Thm.eq_thm (th1, th2));
 
 fun lookup_rule (rs: rules) name = Library.assoc (NetRules.rules rs, name);