src/ZF/Tools/typechk.ML
changeset 42439 9efdd0af15ac
parent 38522 de7984a7172b
child 42795 66fcc9882784
     1.1 --- a/src/ZF/Tools/typechk.ML	Wed Apr 20 17:17:01 2011 +0200
     1.2 +++ b/src/ZF/Tools/typechk.ML	Wed Apr 20 22:57:29 2011 +0200
     1.3 @@ -25,20 +25,17 @@
     1.4   {rules: thm list,     (*the type-checking rules*)
     1.5    net: thm Net.net};   (*discrimination net of the same rules*)
     1.6  
     1.7 -fun add_rule th (tcs as TC {rules, net}) =
     1.8 +fun add_rule ctxt th (tcs as TC {rules, net}) =
     1.9    if member Thm.eq_thm_prop rules th then
    1.10 -    (warning ("Ignoring duplicate type-checking rule\n" ^
    1.11 -        Display.string_of_thm_without_context th); tcs)
    1.12 +    (warning ("Ignoring duplicate type-checking rule\n" ^ Display.string_of_thm ctxt th); tcs)
    1.13    else
    1.14 -    TC {rules = th :: rules,
    1.15 -        net = Net.insert_term (K false) (Thm.concl_of th, th) net};
    1.16 +    TC {rules = th :: rules, net = Net.insert_term (K false) (Thm.concl_of th, th) net};
    1.17  
    1.18 -fun del_rule th (tcs as TC {rules, net}) =
    1.19 +fun del_rule ctxt th (tcs as TC {rules, net}) =
    1.20    if member Thm.eq_thm_prop rules th then
    1.21      TC {net = Net.delete_term Thm.eq_thm_prop (Thm.concl_of th, th) net,
    1.22 -        rules = remove Thm.eq_thm_prop th rules}
    1.23 -  else (warning ("No such type-checking rule\n" ^
    1.24 -    Display.string_of_thm_without_context th); tcs);
    1.25 +      rules = remove Thm.eq_thm_prop th rules}
    1.26 +  else (warning ("No such type-checking rule\n" ^ Display.string_of_thm ctxt th); tcs);
    1.27  
    1.28  
    1.29  (* generic data *)
    1.30 @@ -52,8 +49,13 @@
    1.31      TC {rules = Thm.merge_thms (rules, rules'), net = Net.merge Thm.eq_thm_prop (net, net')};
    1.32  );
    1.33  
    1.34 -val TC_add = Thm.declaration_attribute (Data.map o add_rule);
    1.35 -val TC_del = Thm.declaration_attribute (Data.map o del_rule);
    1.36 +val TC_add =
    1.37 +  Thm.declaration_attribute (fn thm => fn context =>
    1.38 +    Data.map (add_rule (Context.proof_of context) thm) context);
    1.39 +
    1.40 +val TC_del =
    1.41 +  Thm.declaration_attribute (fn thm => fn context =>
    1.42 +    Data.map (del_rule (Context.proof_of context) thm) context);
    1.43  
    1.44  val tcset_of = Data.get o Context.Proof;
    1.45