fixed ML;
authorwenzelm
Thu Sep 15 17:17:03 2005 +0200 (2005-09-15)
changeset 17415ec859c451f59
parent 17414 c9e9d2a2fc72
child 17416 5093a587da16
fixed ML;
src/HOL/ex/SVC_Oracle.ML
     1.1 --- a/src/HOL/ex/SVC_Oracle.ML	Thu Sep 15 17:17:02 2005 +0200
     1.2 +++ b/src/HOL/ex/SVC_Oracle.ML	Thu Sep 15 17:17:03 2005 +0200
     1.3 @@ -97,8 +97,8 @@
     1.4    let
     1.5      val (abs_goal, _) = svc_abstract (Logic.get_goal (Thm.prop_of st) i)
     1.6      val th = svc_oracle (Thm.theory_of_thm st) abs_goal
     1.7 -   in compose_tac (false, th, 0) i end
     1.8 -   handle TERM _ => no_tac;
     1.9 +   in compose_tac (false, th, 0) i st end
    1.10 +   handle TERM _ => no_tac st;
    1.11  
    1.12  
    1.13  (*check if user has SVC installed*)