# HG changeset patch
# User wenzelm
# Date 1150565866 -7200
# Node ID 7f480338b66e11ebdfc3700d726d78abd4eca6bb
# Parent  9956ecabd9afedfb4136de0d88ce508efe55a192
ProofContext.export: singleton;

diff -r 9956ecabd9af -r 7f480338b66e src/Provers/project_rule.ML
--- a/src/Provers/project_rule.ML	Sat Jun 17 19:37:45 2006 +0200
+++ b/src/Provers/project_rule.ML	Sat Jun 17 19:37:46 2006 +0200
@@ -43,7 +43,7 @@
       |> proj i
       |> prems 0 |-> (fn k =>
         Thm.permute_prems 0 (~ k)
-        #> ProofContext.export ctxt' ctxt
+        #> singleton (Variable.export ctxt' ctxt)
         #> Drule.zero_var_indexes
         #> RuleCases.save raw_rule
         #> RuleCases.add_consumes k);