diff -r 7b19666f0e3d -r ecf6375e2abb src/HOL/ex/SVC_Oracle.thy
--- a/src/HOL/ex/SVC_Oracle.thy	Sat Jan 14 19:06:05 2012 +0100
+++ b/src/HOL/ex/SVC_Oracle.thy	Sat Jan 14 20:05:58 2012 +0100
@@ -101,7 +101,7 @@
     fun mt ((c as Const(@{const_name Trueprop}, _)) $ p) = c $ (fm p)
       | mt ((c as Const("==>", _)) $ p $ q)  = c $ (mt p) $ (mt q)
       | mt t = fm t  (*it might be a formula*)
-  in (list_all (params, mt body), !pairs) end;
+  in (Logic.list_all (params, mt body), !pairs) end;
 
 
 (*Present the entire subgoal to the oracle, assumptions and all, but possibly