# HG changeset patch
# User wenzelm
# Date 1441224151 -7200
# Node ID 3d88cd531abe8f4b49a2fea829e4b0ccf65626d0
# Parent  0f48b7b80e887e419573edbf7e57320351e67e97
trim context for persistent storage;
clarified thm equality;

diff -r 0f48b7b80e88 -r 3d88cd531abe src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Wed Sep 02 21:54:32 2015 +0200
+++ b/src/Pure/Proof/extraction.ML	Wed Sep 02 22:02:31 2015 +0200
@@ -399,7 +399,7 @@
          typeof_eqns = add_rule ([], Logic.dest_equals (map_types
            Type.strip_sorts (Thm.prop_of (Drule.abs_def thm)))) typeof_eqns,
          types = types,
-         realizers = realizers, defs = insert Thm.eq_thm thm defs,
+         realizers = realizers, defs = insert Thm.eq_thm_prop (Thm.trim_context thm) defs,
          expand = expand, prep = prep}
       else
         {realizes_eqns = realizes_eqns, typeof_eqns = typeof_eqns, types = types,
@@ -486,7 +486,8 @@
     val procs = maps (rev o fst o snd) types;
     val rtypes = map fst types;
     val typroc = typeof_proc [];
-    val prep = the_default (K I) prep thy' o ProofRewriteRules.elim_defs thy' false defs o
+    val prep = the_default (K I) prep thy' o
+      ProofRewriteRules.elim_defs thy' false (map (Thm.transfer thy) defs) o
       Reconstruct.expand_proof thy' (map (rpair NONE) ("" :: expand));
     val rrews = Net.merge (K false) (#net realizes_eqns, #net typeof_eqns);