src/ZF/Tools/typechk.ML
changeset 32091 30e2ffbba718
parent 30722 623d4831c8cf
child 32170 541b35729992
     1.1 --- a/src/ZF/Tools/typechk.ML	Tue Jul 21 00:56:19 2009 +0200
     1.2 +++ b/src/ZF/Tools/typechk.ML	Tue Jul 21 01:03:18 2009 +0200
     1.3 @@ -27,7 +27,8 @@
     1.4  
     1.5  fun add_rule th (tcs as TC {rules, net}) =
     1.6    if member Thm.eq_thm_prop rules th then
     1.7 -    (warning ("Ignoring duplicate type-checking rule\n" ^ Display.string_of_thm th); tcs)
     1.8 +    (warning ("Ignoring duplicate type-checking rule\n" ^
     1.9 +        Display.string_of_thm_without_context 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 @@ -36,7 +37,8 @@
    1.14    if member Thm.eq_thm_prop rules th then
    1.15      TC {net = Net.delete_term Thm.eq_thm_prop (Thm.concl_of th, th) net,
    1.16          rules = remove Thm.eq_thm_prop th rules}
    1.17 -  else (warning ("No such type-checking rule\n" ^ Display.string_of_thm th); tcs);
    1.18 +  else (warning ("No such type-checking rule\n" ^
    1.19 +    Display.string_of_thm_without_context th); tcs);
    1.20  
    1.21  
    1.22  (* generic data *)
    1.23 @@ -60,7 +62,7 @@
    1.24  fun print_tcset ctxt =
    1.25    let val TC {rules, ...} = tcset_of ctxt in
    1.26      Pretty.writeln (Pretty.big_list "type-checking rules:"
    1.27 -      (map (ProofContext.pretty_thm ctxt) rules))
    1.28 +      (map (Display.pretty_thm ctxt) rules))
    1.29    end;
    1.30  
    1.31