src/Provers/classical.ML
changeset 26928 ca87aff1ad2d
parent 26497 1873915c64a9
child 26938 64e850c3da9e
     1.1 --- a/src/Provers/classical.ML	Fri May 16 23:25:37 2008 +0200
     1.2 +++ b/src/Provers/classical.ML	Sat May 17 13:54:30 2008 +0200
     1.3 @@ -338,13 +338,13 @@
     1.4    is still allowed.*)
     1.5  fun warn_dup th (CS{safeIs, safeEs, hazIs, hazEs, ...}) =
     1.6         if mem_thm safeIs th then
     1.7 -         warning ("Rule already declared as safe introduction (intro!)\n" ^ string_of_thm th)
     1.8 +         warning ("Rule already declared as safe introduction (intro!)\n" ^ Display.string_of_thm th)
     1.9    else if mem_thm safeEs th then
    1.10 -         warning ("Rule already declared as safe elimination (elim!)\n" ^ string_of_thm th)
    1.11 +         warning ("Rule already declared as safe elimination (elim!)\n" ^ Display.string_of_thm th)
    1.12    else if mem_thm hazIs th then
    1.13 -         warning ("Rule already declared as introduction (intro)\n" ^ string_of_thm th)
    1.14 +         warning ("Rule already declared as introduction (intro)\n" ^ Display.string_of_thm th)
    1.15    else if mem_thm hazEs th then
    1.16 -         warning ("Rule already declared as elimination (elim)\n" ^ string_of_thm th)
    1.17 +         warning ("Rule already declared as elimination (elim)\n" ^ Display.string_of_thm th)
    1.18    else ();
    1.19  
    1.20  
    1.21 @@ -354,7 +354,7 @@
    1.22    (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
    1.23               safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
    1.24    if mem_thm safeIs th then
    1.25 -         (warning ("Ignoring duplicate safe introduction (intro!)\n" ^ string_of_thm th);
    1.26 +         (warning ("Ignoring duplicate safe introduction (intro!)\n" ^ Display.string_of_thm th);
    1.27            cs)
    1.28    else
    1.29    let val th' = flat_rule th
    1.30 @@ -380,10 +380,10 @@
    1.31    (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
    1.32               safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
    1.33    if mem_thm safeEs th then
    1.34 -         (warning ("Ignoring duplicate safe elimination (elim!)\n" ^ string_of_thm th);
    1.35 +         (warning ("Ignoring duplicate safe elimination (elim!)\n" ^ Display.string_of_thm th);
    1.36            cs)
    1.37    else if has_fewer_prems 1 th then
    1.38 -    	error("Ill-formed elimination rule\n" ^ string_of_thm th)
    1.39 +    	error("Ill-formed elimination rule\n" ^ Display.string_of_thm th)
    1.40    else
    1.41    let
    1.42        val th' = classical_rule (flat_rule th)
    1.43 @@ -410,7 +410,7 @@
    1.44  
    1.45  fun make_elim th =
    1.46      if has_fewer_prems 1 th then
    1.47 -    	error("Ill-formed destruction rule\n" ^ string_of_thm th)
    1.48 +    	error("Ill-formed destruction rule\n" ^ Display.string_of_thm th)
    1.49      else Tactic.make_elim th;
    1.50  
    1.51  fun cs addSDs ths = cs addSEs (map make_elim ths);
    1.52 @@ -422,7 +422,7 @@
    1.53    (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
    1.54               safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
    1.55    if mem_thm hazIs th then
    1.56 -         (warning ("Ignoring duplicate introduction (intro)\n" ^ string_of_thm th);
    1.57 +         (warning ("Ignoring duplicate introduction (intro)\n" ^ Display.string_of_thm th);
    1.58            cs)
    1.59    else
    1.60    let val th' = flat_rule th
    1.61 @@ -442,16 +442,16 @@
    1.62          xtra_netpair = insert' (the_default 1 w) (nI,nE) ([th], []) xtra_netpair}
    1.63    end
    1.64    handle THM("RSN: no unifiers",_,_) => (*from dup_intr*)
    1.65 -         error ("Ill-formed introduction rule\n" ^ string_of_thm th);
    1.66 +         error ("Ill-formed introduction rule\n" ^ Display.string_of_thm th);
    1.67  
    1.68  fun addE w th
    1.69    (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
    1.70              safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
    1.71    if mem_thm hazEs th then
    1.72 -         (warning ("Ignoring duplicate elimination (elim)\n" ^ string_of_thm th);
    1.73 +         (warning ("Ignoring duplicate elimination (elim)\n" ^ Display.string_of_thm th);
    1.74            cs)
    1.75    else if has_fewer_prems 1 th then
    1.76 -    	error("Ill-formed elimination rule\n" ^ string_of_thm th)
    1.77 +    	error("Ill-formed elimination rule\n" ^ Display.string_of_thm th)
    1.78    else
    1.79    let
    1.80        val th' = classical_rule (flat_rule th)
    1.81 @@ -543,7 +543,7 @@
    1.82      end
    1.83   else cs
    1.84   handle THM("RSN: no unifiers",_,_) => (*from dup_intr*)
    1.85 -        error ("Ill-formed introduction rule\n" ^ string_of_thm th);
    1.86 +        error ("Ill-formed introduction rule\n" ^ Display.string_of_thm th);
    1.87  
    1.88  
    1.89  fun delE th
    1.90 @@ -572,7 +572,7 @@
    1.91        mem_thm hazIs th orelse mem_thm hazEs th orelse
    1.92        mem_thm safeEs th' orelse mem_thm hazEs th'
    1.93      then delSI th (delSE th (delI th (delE th (delSE th' (delE th' cs)))))
    1.94 -    else (warning ("Undeclared classical rule\n" ^ string_of_thm th); cs)
    1.95 +    else (warning ("Undeclared classical rule\n" ^ Display.string_of_thm th); cs)
    1.96    end;
    1.97  
    1.98  fun cs delrules ths = fold delrule ths cs;