--- a/src/Provers/classical.ML Fri May 16 23:25:37 2008 +0200
+++ b/src/Provers/classical.ML Sat May 17 13:54:30 2008 +0200
@@ -338,13 +338,13 @@
is still allowed.*)
fun warn_dup th (CS{safeIs, safeEs, hazIs, hazEs, ...}) =
if mem_thm safeIs th then
- warning ("Rule already declared as safe introduction (intro!)\n" ^ string_of_thm th)
+ warning ("Rule already declared as safe introduction (intro!)\n" ^ Display.string_of_thm th)
else if mem_thm safeEs th then
- warning ("Rule already declared as safe elimination (elim!)\n" ^ string_of_thm th)
+ warning ("Rule already declared as safe elimination (elim!)\n" ^ Display.string_of_thm th)
else if mem_thm hazIs th then
- warning ("Rule already declared as introduction (intro)\n" ^ string_of_thm th)
+ warning ("Rule already declared as introduction (intro)\n" ^ Display.string_of_thm th)
else if mem_thm hazEs th then
- warning ("Rule already declared as elimination (elim)\n" ^ string_of_thm th)
+ warning ("Rule already declared as elimination (elim)\n" ^ Display.string_of_thm th)
else ();
@@ -354,7 +354,7 @@
(cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
if mem_thm safeIs th then
- (warning ("Ignoring duplicate safe introduction (intro!)\n" ^ string_of_thm th);
+ (warning ("Ignoring duplicate safe introduction (intro!)\n" ^ Display.string_of_thm th);
cs)
else
let val th' = flat_rule th
@@ -380,10 +380,10 @@
(cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
if mem_thm safeEs th then
- (warning ("Ignoring duplicate safe elimination (elim!)\n" ^ string_of_thm th);
+ (warning ("Ignoring duplicate safe elimination (elim!)\n" ^ Display.string_of_thm th);
cs)
else if has_fewer_prems 1 th then
- error("Ill-formed elimination rule\n" ^ string_of_thm th)
+ error("Ill-formed elimination rule\n" ^ Display.string_of_thm th)
else
let
val th' = classical_rule (flat_rule th)
@@ -410,7 +410,7 @@
fun make_elim th =
if has_fewer_prems 1 th then
- error("Ill-formed destruction rule\n" ^ string_of_thm th)
+ error("Ill-formed destruction rule\n" ^ Display.string_of_thm th)
else Tactic.make_elim th;
fun cs addSDs ths = cs addSEs (map make_elim ths);
@@ -422,7 +422,7 @@
(cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
if mem_thm hazIs th then
- (warning ("Ignoring duplicate introduction (intro)\n" ^ string_of_thm th);
+ (warning ("Ignoring duplicate introduction (intro)\n" ^ Display.string_of_thm th);
cs)
else
let val th' = flat_rule th
@@ -442,16 +442,16 @@
xtra_netpair = insert' (the_default 1 w) (nI,nE) ([th], []) xtra_netpair}
end
handle THM("RSN: no unifiers",_,_) => (*from dup_intr*)
- error ("Ill-formed introduction rule\n" ^ string_of_thm th);
+ error ("Ill-formed introduction rule\n" ^ Display.string_of_thm th);
fun addE w th
(cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
if mem_thm hazEs th then
- (warning ("Ignoring duplicate elimination (elim)\n" ^ string_of_thm th);
+ (warning ("Ignoring duplicate elimination (elim)\n" ^ Display.string_of_thm th);
cs)
else if has_fewer_prems 1 th then
- error("Ill-formed elimination rule\n" ^ string_of_thm th)
+ error("Ill-formed elimination rule\n" ^ Display.string_of_thm th)
else
let
val th' = classical_rule (flat_rule th)
@@ -543,7 +543,7 @@
end
else cs
handle THM("RSN: no unifiers",_,_) => (*from dup_intr*)
- error ("Ill-formed introduction rule\n" ^ string_of_thm th);
+ error ("Ill-formed introduction rule\n" ^ Display.string_of_thm th);
fun delE th
@@ -572,7 +572,7 @@
mem_thm hazIs th orelse mem_thm hazEs th orelse
mem_thm safeEs th' orelse mem_thm hazEs th'
then delSI th (delSE th (delI th (delE th (delSE th' (delE th' cs)))))
- else (warning ("Undeclared classical rule\n" ^ string_of_thm th); cs)
+ else (warning ("Undeclared classical rule\n" ^ Display.string_of_thm th); cs)
end;
fun cs delrules ths = fold delrule ths cs;