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