diff -r df377a6fdd90 -r 56d2c357e6b5 src/FOL/FOL.thy
--- a/src/FOL/FOL.thy	Fri Mar 20 11:53:22 2015 +0100
+++ b/src/FOL/FOL.thy	Fri Mar 20 14:48:04 2015 +0100
@@ -67,7 +67,7 @@
 
 ML {*
   fun case_tac ctxt a =
-    res_inst_tac ctxt [((("P", 0), Position.none), a)] @{thm case_split}
+    Rule_Insts.res_inst_tac ctxt [((("P", 0), Position.none), a)] @{thm case_split}
 *}
 
 method_setup case_tac = {*