equal
deleted
inserted
replaced
107 |
107 |
108 (*Present the entire subgoal to the oracle, assumptions and all, but possibly |
108 (*Present the entire subgoal to the oracle, assumptions and all, but possibly |
109 abstracted. Use via compose_tac, which performs no lifting but will |
109 abstracted. Use via compose_tac, which performs no lifting but will |
110 instantiate variables.*) |
110 instantiate variables.*) |
111 |
111 |
112 val svc_tac = CSUBGOAL (fn (ct, i) => |
112 fun svc_tac ctxt = CSUBGOAL (fn (ct, i) => |
113 let |
113 let |
114 val thy = Thm.theory_of_cterm ct; |
114 val thy = Thm.theory_of_cterm ct; |
115 val (abs_goal, _) = svc_abstract (Thm.term_of ct); |
115 val (abs_goal, _) = svc_abstract (Thm.term_of ct); |
116 val th = svc_oracle (Thm.cterm_of thy abs_goal); |
116 val th = svc_oracle (Thm.cterm_of thy abs_goal); |
117 in compose_tac (false, th, 0) i end |
117 in compose_tac ctxt (false, th, 0) i end |
118 handle TERM _ => no_tac); |
118 handle TERM _ => no_tac); |
119 *} |
119 *} |
120 |
120 |
|
121 method_setup svc = {* Scan.succeed (SIMPLE_METHOD' o svc_tac) *} |
|
122 |
121 end |
123 end |