# HG changeset patch
# User paulson
# Date 937816808 -7200
# Node ID 680eca63b98e5cce7972b63193e5647cdd4f4c14
# Parent  35787339156179f1643d2a340134a832026b66c3
now uses Pattern.aeconv, not aconv, to test equality between the terms
abstracted over; otherwise it is incomplete.  Other changes are cosmetic

diff -r 357873391561 -r 680eca63b98e src/HOL/SVC_Oracle.ML
--- a/src/HOL/SVC_Oracle.ML	Fri Sep 17 10:31:38 1999 +0200
+++ b/src/HOL/SVC_Oracle.ML	Mon Sep 20 10:40:08 1999 +0200
@@ -5,6 +5,9 @@
 
 Installing the oracle for SVC (Stanford Validity Checker)
 
+The following code merely CALLS the oracle; 
+  the soundness-critical functions are at HOL/Tools/svc_funcs.ML
+
 Based upon the work of Søren T. Heilmann
 *)
 
@@ -13,6 +16,10 @@
   all subterms not intelligible to SVC.*)
 fun svc_abstract t =
   let
+    (*The oracle's result is given to the subgoal using compose_tac because
+      its premises are matched against the assumptions rather than used
+      to make subgoals.  Therefore , abstraction must copy the parameters
+      precisely and make them available to all generated Vars.*)
     val params = Term.strip_all_vars t
     and body   = Term.strip_all_body t
     val Us = map #2 params
@@ -21,7 +28,7 @@
     val pairs = ref ([] : (term*term) list)
     fun insert t = 
 	let val T = fastype_of t
-	    val v = Unify.combound (Var ((!vname,0), Us--->T),
+            val v = Unify.combound (Var ((!vname,0), Us--->T),
 				    0, nPar)
 	in  vname := bump_string (!vname); 
 	    pairs := (t, v) :: !pairs;
@@ -31,7 +38,7 @@
 	case t of
 	    Free _  => t  (*but not existing Vars, lest the names clash*)
 	  | Bound _ => t
-	  | _ => (case gen_assoc (op aconv) (!pairs, t) of
+	  | _ => (case gen_assoc Pattern.aeconv (!pairs, t) of
 		      Some v => v
 		    | None   => insert t)
     (*abstraction of a real/rational expression*)
@@ -72,9 +79,9 @@
       | fm ((c as Const("Not", _)) $ p) = c $ (fm p)
       | fm ((c as Const("True", _))) = c
       | fm ((c as Const("False", _))) = c
-      | fm (t as Const("op =", Type ("fun", [T,_])) $ x $ y) = rel (T, t)
-      | fm (t as Const("op <", Type ("fun", [T,_])) $ x $ y) = rel (T, t)
-      | fm (t as Const("op <=", Type ("fun", [T,_])) $ x $ y) = rel (T, t)
+      | fm (t as Const("op =",  Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
+      | fm (t as Const("op <",  Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
+      | fm (t as Const("op <=", Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
       | fm t = replace t
     (*entry point, and abstraction of a meta-formula*)
     fun mt ((c as Const("Trueprop", _)) $ p) = c $ (fm p)