# HG changeset patch
# User wenzelm
# Date 1126797423 -7200
# Node ID ec859c451f59678da5b0ed13bf3009b06e3fa1cc
# Parent  c9e9d2a2fc72e0aa4905de8a0f2fab5844baabfc
fixed ML;

diff -r c9e9d2a2fc72 -r ec859c451f59 src/HOL/ex/SVC_Oracle.ML
--- a/src/HOL/ex/SVC_Oracle.ML	Thu Sep 15 17:17:02 2005 +0200
+++ b/src/HOL/ex/SVC_Oracle.ML	Thu Sep 15 17:17:03 2005 +0200
@@ -97,8 +97,8 @@
   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 end
-   handle TERM _ => no_tac;
+   in compose_tac (false, th, 0) i st end
+   handle TERM _ => no_tac st;
 
 
 (*check if user has SVC installed*)