equal
deleted
inserted
replaced
134 |
134 |
135 (*Makes a rule by applying a tactic to an existing rule*) |
135 (*Makes a rule by applying a tactic to an existing rule*) |
136 fun rule_by_tactic tac rl = |
136 fun rule_by_tactic tac rl = |
137 let |
137 let |
138 val ctxt = Variable.thm_context rl; |
138 val ctxt = Variable.thm_context rl; |
139 val ([st], ctxt') = Variable.import true [rl] ctxt; |
139 val ((_, [st]), ctxt') = Variable.import true [rl] ctxt; |
140 in |
140 in |
141 (case Seq.pull (tac st) of |
141 (case Seq.pull (tac st) of |
142 NONE => raise THM ("rule_by_tactic", 0, [rl]) |
142 NONE => raise THM ("rule_by_tactic", 0, [rl]) |
143 | SOME (st', _) => zero_var_indexes (singleton (Variable.export ctxt' ctxt) st')) |
143 | SOME (st', _) => zero_var_indexes (singleton (Variable.export ctxt' ctxt) st')) |
144 end; |
144 end; |