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);