--- a/src/HOL/ex/SVC_Oracle.thy Thu Sep 18 14:06:58 2008 +0200
+++ b/src/HOL/ex/SVC_Oracle.thy Thu Sep 18 19:39:44 2008 +0200
@@ -19,8 +19,7 @@
hide const iff_keep iff_unfold
-oracle
- svc_oracle ("term") = Svc.oracle
+oracle svc_oracle = Svc.oracle
ML {*
(*
@@ -110,12 +109,13 @@
abstracted. Use via compose_tac, which performs no lifting but will
instantiate variables.*)
-fun svc_tac i st =
+val svc_tac = CSUBGOAL (fn (ct, i) =>
let
- val (abs_goal, _) = svc_abstract (Logic.get_goal (Thm.prop_of st) i)
- val th = svc_oracle (Thm.theory_of_thm st) abs_goal
- in compose_tac (false, th, 0) i st end
- handle TERM _ => no_tac st;
+ val thy = Thm.theory_of_cterm ct;
+ val (abs_goal, _) = svc_abstract (Thm.term_of ct);
+ val th = svc_oracle (Thm.cterm_of thy abs_goal);
+ in compose_tac (false, th, 0) i end
+ handle TERM _ => no_tac);
*}
end