src/Provers/project_rule.ML
changeset 19905 7f480338b66e
parent 19897 fe661eb3b0e7
child 20218 be3bfb0699ba
equal deleted inserted replaced
19904:9956ecabd9af 19905:7f480338b66e
    41     fun result i =
    41     fun result i =
    42       rule
    42       rule
    43       |> proj i
    43       |> proj i
    44       |> prems 0 |-> (fn k =>
    44       |> prems 0 |-> (fn k =>
    45         Thm.permute_prems 0 (~ k)
    45         Thm.permute_prems 0 (~ k)
    46         #> ProofContext.export ctxt' ctxt
    46         #> singleton (Variable.export ctxt' ctxt)
    47         #> Drule.zero_var_indexes
    47         #> Drule.zero_var_indexes
    48         #> RuleCases.save raw_rule
    48         #> RuleCases.save raw_rule
    49         #> RuleCases.add_consumes k);
    49         #> RuleCases.add_consumes k);
    50   in map result is end;
    50   in map result is end;
    51 
    51