# HG changeset patch
# User wenzelm
# Date 1436129306 -7200
# Node ID 40eef52464f3e82d113dc1cd66476f488b673a17
# Parent  e007aa6a8aa23f374dd414c533d80f1449552eab
clarified context;

diff -r e007aa6a8aa2 -r 40eef52464f3 src/Provers/classical.ML
--- a/src/Provers/classical.ML	Sun Jul 05 22:32:14 2015 +0200
+++ b/src/Provers/classical.ML	Sun Jul 05 22:48:26 2015 +0200
@@ -282,12 +282,12 @@
 fun delete x = delete_tagged_list (joinrules x);
 fun delete' x = delete_tagged_list (joinrules' x);
 
-fun string_of_thm NONE = Display.string_of_thm_without_context
-  | string_of_thm (SOME context) = Display.string_of_thm (Context.proof_of context);
+fun bad_thm (SOME context) msg th =
+      error (msg ^ "\n" ^ Display.string_of_thm (Context.proof_of context) th)
+  | bad_thm NONE msg th = raise THM (msg, 0, [th]);
 
-fun make_elim context th =
-  if has_fewer_prems 1 th then
-    error ("Ill-formed destruction rule\n" ^ string_of_thm context th)
+fun make_elim opt_context th =
+  if has_fewer_prems 1 th then bad_thm opt_context "Ill-formed destruction rule" th
   else Tactic.make_elim th;
 
 fun warn_thm (SOME (Context.Proof ctxt)) msg th =
@@ -295,31 +295,31 @@
       then warning (msg ^ Display.string_of_thm ctxt th) else ()
   | warn_thm _ _ _ = ();
 
-fun warn_rules context msg rules th =
-  Item_Net.member rules th andalso (warn_thm context msg th; true);
+fun warn_rules opt_context msg rules th =
+  Item_Net.member rules th andalso (warn_thm opt_context msg th; true);
 
-fun warn_claset context th (CS {safeIs, safeEs, hazIs, hazEs, ...}) =
-  warn_rules context "Rule already declared as safe introduction (intro!)\n" safeIs th orelse
-  warn_rules context "Rule already declared as safe elimination (elim!)\n" safeEs th orelse
-  warn_rules context "Rule already declared as introduction (intro)\n" hazIs th orelse
-  warn_rules context "Rule already declared as elimination (elim)\n" hazEs th;
+fun warn_claset opt_context th (CS {safeIs, safeEs, hazIs, hazEs, ...}) =
+  warn_rules opt_context "Rule already declared as safe introduction (intro!)\n" safeIs th orelse
+  warn_rules opt_context "Rule already declared as safe elimination (elim!)\n" safeEs th orelse
+  warn_rules opt_context "Rule already declared as introduction (intro)\n" hazIs th orelse
+  warn_rules opt_context "Rule already declared as elimination (elim)\n" hazEs th;
 
 
 (*** Safe rules ***)
 
-fun addSI w context th
+fun addSI w opt_context th
     (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
       safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
-  if warn_rules context "Ignoring duplicate safe introduction (intro!)\n" safeIs th then cs
+  if warn_rules opt_context "Ignoring duplicate safe introduction (intro!)\n" safeIs th then cs
   else
     let
-      val ctxt = default_context context th;
+      val ctxt = default_context opt_context th;
       val th' = flat_rule ctxt th;
       val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*)
         List.partition Thm.no_prems [th'];
       val nI = Item_Net.length safeIs + 1;
       val nE = Item_Net.length safeEs;
-      val _ = warn_claset context th cs;
+      val _ = warn_claset opt_context th cs;
     in
       CS
        {safeIs = Item_Net.update th safeIs,
@@ -335,21 +335,20 @@
         xtra_netpair = insert' (the_default 0 w) (nI,nE) ([th], []) xtra_netpair}
     end;
 
-fun addSE w context th
+fun addSE w opt_context th
     (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
       safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
-  if warn_rules context "Ignoring duplicate safe elimination (elim!)\n" safeEs th then cs
-  else if has_fewer_prems 1 th then
-    error ("Ill-formed elimination rule\n" ^ string_of_thm context th)
+  if warn_rules opt_context "Ignoring duplicate safe elimination (elim!)\n" safeEs th then cs
+  else if has_fewer_prems 1 th then bad_thm opt_context "Ill-formed elimination rule" th
   else
     let
-      val ctxt = default_context context th;
+      val ctxt = default_context opt_context th;
       val th' = classical_rule ctxt (flat_rule ctxt th);
       val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*)
         List.partition (fn rl => Thm.nprems_of rl=1) [th'];
       val nI = Item_Net.length safeIs;
       val nE = Item_Net.length safeEs + 1;
-      val _ = warn_claset context th cs;
+      val _ = warn_claset opt_context th cs;
     in
       CS
        {safeEs = Item_Net.update th safeEs,
@@ -365,22 +364,22 @@
         xtra_netpair = insert' (the_default 0 w) (nI,nE) ([], [th]) xtra_netpair}
     end;
 
-fun addSD w context th = addSE w context (make_elim context th);
+fun addSD w opt_context th = addSE w opt_context (make_elim opt_context th);
 
 
 (*** Hazardous (unsafe) rules ***)
 
-fun addI w context th
+fun addI w opt_context th
     (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
       safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
-  if warn_rules context "Ignoring duplicate introduction (intro)\n" hazIs th then cs
+  if warn_rules opt_context "Ignoring duplicate introduction (intro)\n" hazIs th then cs
   else
     let
-      val ctxt = default_context context th;
+      val ctxt = default_context opt_context th;
       val th' = flat_rule ctxt th;
       val nI = Item_Net.length hazIs + 1;
       val nE = Item_Net.length hazEs;
-      val _ = warn_claset context th cs;
+      val _ = warn_claset opt_context th cs;
     in
       CS
        {hazIs = Item_Net.update th hazIs,
@@ -396,21 +395,20 @@
         xtra_netpair = insert' (the_default 1 w) (nI, nE) ([th], []) xtra_netpair}
     end
     handle THM ("RSN: no unifiers", _, _) => (*from dup_intr*)  (* FIXME !? *)
-      error ("Ill-formed introduction rule\n" ^ string_of_thm context th);
+      bad_thm opt_context "Ill-formed introduction rule" th;
 
-fun addE w context th
+fun addE w opt_context th
     (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
       safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
-  if warn_rules context "Ignoring duplicate elimination (elim)\n" hazEs th then cs
-  else if has_fewer_prems 1 th then
-    error ("Ill-formed elimination rule\n" ^ string_of_thm context th)
+  if warn_rules opt_context "Ignoring duplicate elimination (elim)\n" hazEs th then cs
+  else if has_fewer_prems 1 th then bad_thm opt_context "Ill-formed elimination rule" th
   else
     let
-      val ctxt = default_context context th;
+      val ctxt = default_context opt_context th;
       val th' = classical_rule ctxt (flat_rule ctxt th);
       val nI = Item_Net.length hazIs;
       val nE = Item_Net.length hazEs + 1;
-      val _ = warn_claset context th cs;
+      val _ = warn_claset opt_context th cs;
     in
       CS
        {hazEs = Item_Net.update th hazEs,
@@ -426,7 +424,7 @@
         xtra_netpair = insert' (the_default 1 w) (nI, nE) ([], [th]) xtra_netpair}
     end;
 
-fun addD w context th = addE w context (make_elim context th);
+fun addD w opt_context th = addE w opt_context (make_elim opt_context th);
 
 
 
@@ -435,12 +433,12 @@
         to insert.
 ***)
 
-fun delSI context th
+fun delSI opt_context th
     (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
       safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   if Item_Net.member safeIs th then
     let
-      val ctxt = default_context context th;
+      val ctxt = default_context opt_context th;
       val th' = flat_rule ctxt th;
       val (safe0_rls, safep_rls) = List.partition Thm.no_prems [th'];
     in
@@ -459,12 +457,12 @@
     end
   else cs;
 
-fun delSE context th
+fun delSE opt_context th
     (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
       safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   if Item_Net.member safeEs th then
     let
-      val ctxt = default_context context th;
+      val ctxt = default_context opt_context th;
       val th' = classical_rule ctxt (flat_rule ctxt th);
       val (safe0_rls, safep_rls) = List.partition (fn rl => Thm.nprems_of rl = 1) [th'];
     in
@@ -483,12 +481,12 @@
     end
   else cs;
 
-fun delI context th
+fun delI opt_context th
     (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
       safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   if Item_Net.member hazIs th then
     let
-      val ctxt = default_context context th;
+      val ctxt = default_context opt_context th;
       val th' = flat_rule ctxt th;
     in
       CS
@@ -506,14 +504,14 @@
     end
   else cs
   handle THM ("RSN: no unifiers", _, _) => (*from dup_intr*)  (* FIXME !? *)
-    error ("Ill-formed introduction rule\n" ^ string_of_thm context th);
+    bad_thm opt_context "Ill-formed introduction rule" th;
 
-fun delE context th
+fun delE opt_context th
     (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
       safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   if Item_Net.member hazEs th then
     let
-      val ctxt = default_context context th;
+      val ctxt = default_context opt_context th;
       val th' = classical_rule ctxt (flat_rule ctxt th);
     in
       CS
@@ -532,17 +530,17 @@
   else cs;
 
 (*Delete ALL occurrences of "th" in the claset (perhaps from several lists)*)
-fun delrule context th (cs as CS {safeIs, safeEs, hazIs, hazEs, ...}) =
+fun delrule opt_context th (cs as CS {safeIs, safeEs, hazIs, hazEs, ...}) =
   let val th' = Tactic.make_elim th in
     if Item_Net.member safeIs th orelse Item_Net.member safeEs th orelse
       Item_Net.member hazIs th orelse Item_Net.member hazEs th orelse
       Item_Net.member safeEs th' orelse Item_Net.member hazEs th'
     then
-      delSI context th
-        (delSE context th
-          (delI context th
-            (delE context th (delSE context th' (delE context th' cs)))))
-    else (warn_thm context "Undeclared classical rule\n" th; cs)
+      delSI opt_context th
+        (delSE opt_context th
+          (delI opt_context th
+            (delE opt_context th (delSE opt_context th' (delE opt_context th' cs)))))
+    else (warn_thm opt_context "Undeclared classical rule\n" th; cs)
   end;
 
 
@@ -858,7 +856,8 @@
 (* attributes *)
 
 fun attrib f =
-  Thm.declaration_attribute (fn th => fn context => map_cs (f (SOME context) th) context);
+  Thm.declaration_attribute (fn th => fn opt_context =>
+    map_cs (f (SOME opt_context) th) opt_context);
 
 val safe_elim = attrib o addSE;
 val safe_intro = attrib o addSI;
@@ -868,8 +867,8 @@
 val haz_dest = attrib o addD;
 
 val rule_del =
-  Thm.declaration_attribute (fn th => fn context =>
-    context |> map_cs (delrule (SOME context) th) |>
+  Thm.declaration_attribute (fn th => fn opt_context =>
+    opt_context |> map_cs (delrule (SOME opt_context) th) |>
     Thm.attribute_declaration Context_Rules.rule_del th);