author | wenzelm |
Wed, 05 Dec 2001 03:15:32 +0100 | |
changeset 12381 | 5177845a34f5 |
parent 12380 | 3402d300f5ef |
child 12382 | 8896d7f49422 |
--- 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);