changeset 19905 | 7f480338b66e |
parent 19897 | fe661eb3b0e7 |
child 20218 | be3bfb0699ba |
--- 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);