src/Provers/classical.ML
changeset 32091 30e2ffbba718
parent 31945 d5f186aa0bed
child 32148 253f6808dabe
--- a/src/Provers/classical.ML	Tue Jul 21 00:56:19 2009 +0200
+++ b/src/Provers/classical.ML	Tue Jul 21 01:03:18 2009 +0200
@@ -256,7 +256,7 @@
      xtra_netpair  = empty_netpair};
 
 fun print_cs (CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, ...}) =
-  let val pretty_thms = map Display.pretty_thm in
+  let val pretty_thms = map Display.pretty_thm_without_context in
     [Pretty.big_list "safe introduction rules (intro!):" (pretty_thms safeIs),
       Pretty.big_list "introduction rules (intro):" (pretty_thms hazIs),
       Pretty.big_list "safe elimination rules (elim!):" (pretty_thms safeEs),
@@ -313,14 +313,18 @@
 (*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" ^ Display.string_of_thm th)
+  if mem_thm safeIs th then
+    warning ("Rule already declared as safe introduction (intro!)\n" ^
+      Display.string_of_thm_without_context th)
   else if mem_thm safeEs th then
-         warning ("Rule already declared as safe elimination (elim!)\n" ^ Display.string_of_thm th)
+    warning ("Rule already declared as safe elimination (elim!)\n" ^
+      Display.string_of_thm_without_context th)
   else if mem_thm hazIs th then
-         warning ("Rule already declared as introduction (intro)\n" ^ Display.string_of_thm th)
+    warning ("Rule already declared as introduction (intro)\n" ^
+      Display.string_of_thm_without_context th)
   else if mem_thm hazEs th then
-         warning ("Rule already declared as elimination (elim)\n" ^ Display.string_of_thm th)
+    warning ("Rule already declared as elimination (elim)\n" ^
+      Display.string_of_thm_without_context th)
   else ();
 
 
@@ -330,8 +334,8 @@
   (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" ^ Display.string_of_thm th);
-          cs)
+    (warning ("Ignoring duplicate safe introduction (intro!)\n" ^
+      Display.string_of_thm_without_context th); cs)
   else
   let val th' = flat_rule th
       val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*)
@@ -356,10 +360,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" ^ Display.string_of_thm th);
-          cs)
+    (warning ("Ignoring duplicate safe elimination (elim!)\n" ^
+        Display.string_of_thm_without_context th); cs)
   else if has_fewer_prems 1 th then
-    	error("Ill-formed elimination rule\n" ^ Display.string_of_thm th)
+    	error ("Ill-formed elimination rule\n" ^ Display.string_of_thm_without_context th)
   else
   let
       val th' = classical_rule (flat_rule th)
@@ -386,7 +390,7 @@
 
 fun make_elim th =
     if has_fewer_prems 1 th then
-    	error("Ill-formed destruction rule\n" ^ Display.string_of_thm th)
+    	  error ("Ill-formed destruction rule\n" ^ Display.string_of_thm_without_context th)
     else Tactic.make_elim th;
 
 fun cs addSDs ths = cs addSEs (map make_elim ths);
@@ -398,8 +402,8 @@
   (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" ^ Display.string_of_thm th);
-          cs)
+    (warning ("Ignoring duplicate introduction (intro)\n" ^
+        Display.string_of_thm_without_context th); cs)
   else
   let val th' = flat_rule th
       val nI = length hazIs + 1
@@ -418,16 +422,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" ^ Display.string_of_thm th);
+    error ("Ill-formed introduction rule\n" ^ Display.string_of_thm_without_context 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" ^ Display.string_of_thm th);
-          cs)
+    (warning ("Ignoring duplicate elimination (elim)\n" ^
+        Display.string_of_thm_without_context th); cs)
   else if has_fewer_prems 1 th then
-    	error("Ill-formed elimination rule\n" ^ Display.string_of_thm th)
+    	error("Ill-formed elimination rule\n" ^ Display.string_of_thm_without_context th)
   else
   let
       val th' = classical_rule (flat_rule th)
@@ -519,7 +523,7 @@
     end
  else cs
  handle THM("RSN: no unifiers",_,_) => (*from dup_intr*)
-        error ("Ill-formed introduction rule\n" ^ Display.string_of_thm th);
+   error ("Ill-formed introduction rule\n" ^ Display.string_of_thm_without_context th);
 
 
 fun delE th
@@ -548,7 +552,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" ^ Display.string_of_thm th); cs)
+    else (warning ("Undeclared classical rule\n" ^ Display.string_of_thm_without_context th); cs)
   end;
 
 fun cs delrules ths = fold delrule ths cs;