src/Provers/classical.ML

--- 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;