src/ZF/Tools/typechk.ML
changeset 22360 26ead7ed4f4b
parent 21506 b2a673894ce5
child 22846 fb79144af9a3
     1.1 --- a/src/ZF/Tools/typechk.ML	Mon Feb 26 21:34:16 2007 +0100
     1.2 +++ b/src/ZF/Tools/typechk.ML	Mon Feb 26 23:18:24 2007 +0100
     1.3 @@ -27,16 +27,16 @@
     1.4    net: thm Net.net};   (*discrimination net of the same rules*)
     1.5  
     1.6  fun add_rule th (tcs as TC {rules, net}) =
     1.7 -  if member Drule.eq_thm_prop rules th then
     1.8 +  if member Thm.eq_thm_prop rules th then
     1.9      (warning ("Ignoring duplicate type-checking rule\n" ^ Display.string_of_thm th); tcs)
    1.10    else
    1.11      TC {rules = th :: rules,
    1.12          net = Net.insert_term (K false) (Thm.concl_of th, th) net};
    1.13  
    1.14  fun del_rule th (tcs as TC {rules, net}) =
    1.15 -  if member Drule.eq_thm_prop rules th then
    1.16 -    TC {net = Net.delete_term Drule.eq_thm_prop (Thm.concl_of th, th) net,
    1.17 -        rules = remove Drule.eq_thm_prop th rules}
    1.18 +  if member Thm.eq_thm_prop rules th then
    1.19 +    TC {net = Net.delete_term Thm.eq_thm_prop (Thm.concl_of th, th) net,
    1.20 +        rules = remove Thm.eq_thm_prop th rules}
    1.21    else (warning ("No such type-checking rule\n" ^ Display.string_of_thm th); tcs);
    1.22  
    1.23  
    1.24 @@ -51,7 +51,7 @@
    1.25  
    1.26    fun merge _ (TC {rules, net}, TC {rules = rules', net = net'}) =
    1.27      TC {rules = Drule.merge_rules (rules, rules'),
    1.28 -        net = Net.merge Drule.eq_thm_prop (net, net')};
    1.29 +        net = Net.merge Thm.eq_thm_prop (net, net')};
    1.30  
    1.31    fun print context (TC {rules, ...}) =
    1.32      Pretty.writeln (Pretty.big_list "type-checking rules:"