simplified NetRules;
authorwenzelm
Wed Dec 05 03:15:32 2001 +0100 (2001-12-05 ago)
changeset 123815177845a34f5
parent 12380 3402d300f5ef
child 12382 8896d7f49422
simplified NetRules;
src/Pure/Isar/induct_attrib.ML
     1.1 --- a/src/Pure/Isar/induct_attrib.ML	Wed Dec 05 03:15:15 2001 +0100
     1.2 +++ b/src/Pure/Isar/induct_attrib.ML	Wed Dec 05 03:15:32 2001 +0100
     1.3 @@ -83,8 +83,8 @@
     1.4  
     1.5  type rules = (string * thm) NetRules.T;
     1.6  
     1.7 -val init_rules = NetRules.init (fn ((s1: string, th1), (s2, th2)) => s1 = s2
     1.8 -  andalso Thm.eq_thm (th1, th2)) (K 0);
     1.9 +val init_rules =
    1.10 +  NetRules.init (fn ((s1: string, th1), (s2, th2)) => s1 = s2 andalso Thm.eq_thm (th1, th2));
    1.11  
    1.12  fun lookup_rule (rs: rules) name = Library.assoc (NetRules.rules rs, name);
    1.13