src/Pure/Isar/induct_attrib.ML
changeset 13105 3d1e7a199bdc
parent 12381 5177845a34f5
child 14981 e73f8140af78
     1.1 --- a/src/Pure/Isar/induct_attrib.ML	Tue May 07 14:24:30 2002 +0200
     1.2 +++ b/src/Pure/Isar/induct_attrib.ML	Tue May 07 14:26:32 2002 +0200
     1.3 @@ -84,7 +84,8 @@
     1.4  type rules = (string * thm) NetRules.T;
     1.5  
     1.6  val init_rules =
     1.7 -  NetRules.init (fn ((s1: string, th1), (s2, th2)) => s1 = s2 andalso Thm.eq_thm (th1, th2));
     1.8 +  NetRules.init (fn ((s1: string, th1), (s2, th2)) => s1 = s2 andalso
     1.9 +    Drule.eq_thm_prop (th1, th2));
    1.10  
    1.11  fun lookup_rule (rs: rules) name = Library.assoc (NetRules.rules rs, name);
    1.12