1.1 --- a/src/HOL/ex/SVC_Oracle.ML	Thu Jul 14 19:28:17 2005 +0200
     1.2 +++ b/src/HOL/ex/SVC_Oracle.ML	Thu Jul 14 19:28:18 2005 +0200
     1.3 @@ -5,7 +5,7 @@
     1.4  
     1.5  Installing the oracle for SVC (Stanford Validity Checker)
     1.6  
     1.7 -The following code merely CALLS the oracle; 
     1.8 +The following code merely CALLS the oracle;
     1.9    the soundness-critical functions are at HOL/Tools/svc_funcs.ML
    1.10  
    1.11  Based upon the work of Søren T. Heilmann
    1.12 @@ -26,21 +26,21 @@
    1.13      val nPar = length params
    1.14      val vname = ref "V_a"
    1.15      val pairs = ref ([] : (term*term) list)
    1.16 -    fun insert t = 
    1.17 -	let val T = fastype_of t
    1.18 +    fun insert t =
    1.19 +        let val T = fastype_of t
    1.20              val v = Unify.combound (Var ((!vname,0), Us--->T),
    1.21 -				    0, nPar)
    1.22 -	in  vname := Symbol.bump_string (!vname); 
    1.23 -	    pairs := (t, v) :: !pairs;
    1.24 -	    v
    1.25 -	end;
    1.26 -    fun replace t = 
    1.27 -	case t of
    1.28 -	    Free _  => t  (*but not existing Vars, lest the names clash*)
    1.29 -	  | Bound _ => t
    1.30 -	  | _ => (case gen_assoc Pattern.aeconv (!pairs, t) of
    1.31 -		      SOME v => v
    1.32 -		    | NONE   => insert t)
    1.33 +                                    0, nPar)
    1.34 +        in  vname := Symbol.bump_string (!vname);
    1.35 +            pairs := (t, v) :: !pairs;
    1.36 +            v
    1.37 +        end;
    1.38 +    fun replace t =
    1.39 +        case t of
    1.40 +            Free _  => t  (*but not existing Vars, lest the names clash*)
    1.41 +          | Bound _ => t
    1.42 +          | _ => (case gen_assoc Pattern.aeconv (!pairs, t) of
    1.43 +                      SOME v => v
    1.44 +                    | NONE   => insert t)
    1.45      (*abstraction of a numeric literal*)
    1.46      fun lit (t as Const("0", _)) = t
    1.47        | lit (t as Const("1", _)) = t
    1.48 @@ -66,11 +66,11 @@
    1.49        | nat t = lit t
    1.50      (*abstraction of a relation: =, <, <=*)
    1.51      fun rel (T, c $ x $ y) =
    1.52 -	    if T = HOLogic.realT then c $ (rat x) $ (rat y)
    1.53 -	    else if T = HOLogic.intT then c $ (int x) $ (int y)
    1.54 -	    else if T = HOLogic.natT then c $ (nat x) $ (nat y)
    1.55 -	    else if T = HOLogic.boolT then c $ (fm x) $ (fm y)
    1.56 -	    else replace (c $ x $ y)   (*non-numeric comparison*)
    1.57 +            if T = HOLogic.realT then c $ (rat x) $ (rat y)
    1.58 +            else if T = HOLogic.intT then c $ (int x) $ (int y)
    1.59 +            else if T = HOLogic.natT then c $ (nat x) $ (nat y)
    1.60 +            else if T = HOLogic.boolT then c $ (fm x) $ (fm y)
    1.61 +            else replace (c $ x $ y)   (*non-numeric comparison*)
    1.62      (*abstraction of a formula*)
    1.63      and fm ((c as Const("op &", _)) $ p $ q) = c $ (fm p) $ (fm q)
    1.64        | fm ((c as Const("op |", _)) $ p $ q) = c $ (fm p) $ (fm q)
    1.65 @@ -92,20 +92,13 @@
    1.66  (*Present the entire subgoal to the oracle, assumptions and all, but possibly
    1.67    abstracted.  Use via compose_tac, which performs no lifting but will
    1.68    instantiate variables.*)
    1.69 -local val svc_thy = the_context () in
    1.70  
    1.71 -fun svc_tac i st = 
    1.72 -  let val prem = BasisLibrary.List.nth (prems_of st, i-1)
    1.73 -      val (absPrem, _) = svc_abstract prem
    1.74 -      val th = invoke_oracle svc_thy "svc_oracle"
    1.75 -	             (#sign (rep_thm st), Svc.OracleExn absPrem)
    1.76 -   in 
    1.77 -      compose_tac (false, th, 0) i st
    1.78 -   end 
    1.79 -   handle Svc.OracleExn _ => Seq.empty
    1.80 -	| Subscript       => Seq.empty;
    1.81 -
    1.82 -end;
    1.83 +fun svc_tac i st =
    1.84 +  let
    1.85 +    val (abs_goal, _) = svc_abstract (Logic.get_goal (Thm.prop_of st) i)
    1.86 +    val th = svc_oracle (Thm.theory_of_thm st) abs_goal
    1.87 +   in compose_tac (false, th, 0) i end
    1.88 +   handle TERM _ => no_tac;
    1.89  
    1.90  
    1.91  (*check if user has SVC installed*)