src/FOL/FOL.thy

--- a/src/FOL/FOL.thy	Thu Mar 19 17:25:57 2015 +0100
+++ b/src/FOL/FOL.thy	Thu Mar 19 22:30:57 2015 +0100
@@ -66,7 +66,8 @@
   done
 
 ML {*
-  fun case_tac ctxt a = res_inst_tac ctxt [(("P", 0), a)] @{thm case_split}
+  fun case_tac ctxt a =
+    res_inst_tac ctxt [((("P", 0), Position.none), a)] @{thm case_split}
 *}
 
 method_setup case_tac = {*