src/HOL/ex/SVC_Oracle.thy
changeset 28290 4cc2b6046258
parent 28263 69eaa97e7e96
child 32740 9dd0a2f83429
     1.1 --- a/src/HOL/ex/SVC_Oracle.thy	Thu Sep 18 14:06:58 2008 +0200
     1.2 +++ b/src/HOL/ex/SVC_Oracle.thy	Thu Sep 18 19:39:44 2008 +0200
     1.3 @@ -19,8 +19,7 @@
     1.4  
     1.5  hide const iff_keep iff_unfold
     1.6  
     1.7 -oracle
     1.8 -  svc_oracle ("term") = Svc.oracle
     1.9 +oracle svc_oracle = Svc.oracle
    1.10  
    1.11  ML {*
    1.12  (*
    1.13 @@ -110,12 +109,13 @@
    1.14    abstracted.  Use via compose_tac, which performs no lifting but will
    1.15    instantiate variables.*)
    1.16  
    1.17 -fun svc_tac i st =
    1.18 +val svc_tac = CSUBGOAL (fn (ct, i) =>
    1.19    let
    1.20 -    val (abs_goal, _) = svc_abstract (Logic.get_goal (Thm.prop_of st) i)
    1.21 -    val th = svc_oracle (Thm.theory_of_thm st) abs_goal
    1.22 -   in compose_tac (false, th, 0) i st end
    1.23 -   handle TERM _ => no_tac st;
    1.24 +    val thy = Thm.theory_of_cterm ct;
    1.25 +    val (abs_goal, _) = svc_abstract (Thm.term_of ct);
    1.26 +    val th = svc_oracle (Thm.cterm_of thy abs_goal);
    1.27 +   in compose_tac (false, th, 0) i end
    1.28 +   handle TERM _ => no_tac);
    1.29  *}
    1.30  
    1.31  end