src/Provers/classical.ML

 
 (*Warn if the rule is already present ELSEWHERE in the claset.  The addition
   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 ();
 
 
 (*** Safe rules ***)
 
 fun addSI w th
   (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
       val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*)
           List.partition Thm.no_prems [th']

 
 fun addSE w th
   (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)
       val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*)
           List.partition (fn rl => nprems_of rl=1) [th']

 fun cs addSIs ths = fold_rev (addSI NONE) ths cs;
 fun cs addSEs ths = fold_rev (addSE NONE) ths cs;
 
 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);
 
 

 
 fun addI w th
   (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
       val nI = length hazIs + 1
       and nE = length hazEs

         safe0_netpair = safe0_netpair,
         safep_netpair = safep_netpair,
         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)
       val nI = length hazIs
       and nE = length hazEs + 1

         safep_netpair = safep_netpair,
         xtra_netpair = delete' ([th], []) xtra_netpair}
     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
          (cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
                    safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =

   let val th' = Tactic.make_elim th in
     if mem_thm safeIs th orelse mem_thm safeEs th orelse
       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;