# HG changeset patch
# User wenzelm
# Date 1440961054 -7200
# Node ID e9d08b88d2cc91794fb5d2d4a010d7a9f336b13c
# Parent  6fc78876f9be7e701dfe4a5d6c4e1ca495d6e75b
trim context for persistent storage;

diff -r 6fc78876f9be -r e9d08b88d2cc src/Provers/blast.ML
--- a/src/Provers/blast.ML	Sun Aug 30 20:17:35 2015 +0200
+++ b/src/Provers/blast.ML	Sun Aug 30 20:57:34 2015 +0200
@@ -497,24 +497,25 @@
 (*Tableau rule from elimination rule.
   Flag "upd" says that the inference updated the branch.
   Flag "dup" requests duplication of the affected formula.*)
-fun fromRule (state as State {ctxt, ...}) vars rl =
-  let val thy = Proof_Context.theory_of ctxt
-      val trl = rl |> Thm.prop_of |> fromTerm thy |> convertRule state vars
-      fun tac (upd, dup,rot) i =
-        emtac ctxt upd (if dup then rev_dup_elim ctxt rl else rl) i
-        THEN
-        rot_subgoals_tac (rot, #2 trl) i
-  in Option.SOME (trl, tac) end
+fun fromRule (state as State {ctxt, ...}) vars rl0 =
+  let
+    val thy = Proof_Context.theory_of ctxt
+    val rl = Thm.transfer thy rl0
+    val trl = rl |> Thm.prop_of |> fromTerm thy |> convertRule state vars
+    fun tac (upd, dup,rot) i =
+      emtac ctxt upd (if dup then rev_dup_elim ctxt rl else rl) i THEN
+      rot_subgoals_tac (rot, #2 trl) i
+  in SOME (trl, tac) end
   handle
     ElimBadPrem => (*reject: prems don't preserve conclusion*)
       (if Context_Position.is_visible ctxt then
-        warning ("Ignoring weak elimination rule\n" ^ Display.string_of_thm ctxt rl)
+        warning ("Ignoring weak elimination rule\n" ^ Display.string_of_thm ctxt rl0)
        else ();
        Option.NONE)
   | ElimBadConcl => (*ignore: conclusion is not just a variable*)
       (cond_tracing (Config.get ctxt trace)
         (fn () => "Ignoring ill-formed elimination rule:\n" ^
-          "conclusion should be a variable\n" ^ Display.string_of_thm ctxt rl);
+          "conclusion should be a variable\n" ^ Display.string_of_thm ctxt rl0);
        Option.NONE);
 
 
@@ -533,13 +534,14 @@
   Flag "dup" requests duplication of the affected formula.
   Since unsafe rules are now delayed, "dup" is always FALSE for
   introduction rules.*)
-fun fromIntrRule (state as State {ctxt, ...}) vars rl =
-  let val thy = Proof_Context.theory_of ctxt
-      val trl = rl |> Thm.prop_of |> fromTerm thy |> convertIntrRule state vars
-      fun tac (upd,dup,rot) i =
-         rmtac ctxt upd (if dup then Classical.dup_intr rl else rl) i
-         THEN
-         rot_subgoals_tac (rot, #2 trl) i
+fun fromIntrRule (state as State {ctxt, ...}) vars rl0 =
+  let
+    val thy = Proof_Context.theory_of ctxt
+    val rl = Thm.transfer thy rl0
+    val trl = rl |> Thm.prop_of |> fromTerm thy |> convertIntrRule state vars
+    fun tac (upd,dup,rot) i =
+      rmtac ctxt upd (if dup then Classical.dup_intr rl else rl) i THEN
+      rot_subgoals_tac (rot, #2 trl) i
   in (trl, tac) end;
 
 
diff -r 6fc78876f9be -r e9d08b88d2cc src/Provers/classical.ML
--- a/src/Provers/classical.ML	Sun Aug 30 20:17:35 2015 +0200
+++ b/src/Provers/classical.ML	Sun Aug 30 20:57:34 2015 +0200
@@ -193,7 +193,10 @@
 (*Uses introduction rules in the normal way, or on negated assumptions,
   trying rules in order. *)
 fun swap_res_tac ctxt rls =
-  let fun addrl rl brls = (false, rl) :: (true, rl RSN (2, Data.swap)) :: brls in
+  let
+    val transfer = Thm.transfer (Proof_Context.theory_of ctxt);
+    fun addrl rl brls = (false, transfer rl) :: (true, transfer rl RSN (2, Data.swap)) :: brls;
+  in
     assume_tac ctxt ORELSE'
     contr_tac ctxt ORELSE'
     biresolve_tac ctxt (fold_rev addrl rls [])
@@ -401,11 +404,16 @@
         extra_netpair = insert' (the_default 1 w) (nI, nE) ([], [th]) extra_netpair}
     end;
 
+fun trim_context (th, (th1, ths1), (th2, ths2)) =
+  (Thm.trim_context th,
+    (Thm.trim_context th1, map Thm.trim_context ths1),
+    (Thm.trim_context th2, map Thm.trim_context ths2));
+
 fun addSI w ctxt th (cs as CS {safeIs, ...}) =
   let
     val th' = flat_rule ctxt th;
     val rl = (th', swapify [th']);
-    val r = (th, rl, rl);
+    val r = trim_context (th, rl, rl);
     val _ =
       warn_rules ctxt "Ignoring duplicate safe introduction (intro!)\n" safeIs r orelse
       warn_claset ctxt r cs;
@@ -416,7 +424,7 @@
     val _ = has_fewer_prems 1 th andalso bad_thm ctxt "Ill-formed elimination rule" th;
     val th' = classical_rule ctxt (flat_rule ctxt th);
     val rl = (th', []);
-    val r = (th, rl, rl);
+    val r = trim_context (th, rl, rl);
     val _ =
       warn_rules ctxt "Ignoring duplicate safe elimination (elim!)\n" safeEs r orelse
       warn_claset ctxt r cs;
@@ -428,7 +436,7 @@
   let
     val th' = flat_rule ctxt th;
     val dup_th' = dup_intr th' handle THM _ => bad_thm ctxt "Ill-formed introduction rule" th;
-    val r = (th, (th', swapify [th']), (dup_th', swapify [dup_th']));
+    val r = trim_context (th, (th', swapify [th']), (dup_th', swapify [dup_th']));
     val _ =
       warn_rules ctxt "Ignoring duplicate introduction (intro)\n" unsafeIs r orelse
       warn_claset ctxt r cs;
@@ -439,7 +447,7 @@
     val _ = has_fewer_prems 1 th andalso bad_thm ctxt "Ill-formed elimination rule" th;
     val th' = classical_rule ctxt (flat_rule ctxt th);
     val dup_th' = dup_elim ctxt th' handle THM _ => bad_thm ctxt "Ill-formed elimination rule" th;
-    val r = (th, (th', []), (dup_th', []));
+    val r = trim_context (th, (th', []), (dup_th', []));
     val _ =
       warn_rules ctxt "Ignoring duplicate elimination (elim)\n" unsafeEs r orelse
       warn_claset ctxt r cs;