equal
deleted
inserted
replaced
111 |
111 |
112 fun svc_tac ctxt = 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.global_cterm_of thy abs_goal); |
117 in compose_tac ctxt (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) *} |
121 method_setup svc = {* Scan.succeed (SIMPLE_METHOD' o svc_tac) *} |