src/FOL/FOL.thy

--- a/src/FOL/FOL.thy	Mon Jun 16 17:56:08 2008 +0200
+++ b/src/FOL/FOL.thy	Mon Jun 16 22:13:39 2008 +0200
@@ -70,8 +70,7 @@
   done
 
 ML {*
-  fun case_tac ctxt a =
-    RuleInsts.res_inst_tac ctxt [(("P", 0), a)] @{thm case_split}
+  fun case_tac ctxt a = res_inst_tac ctxt [(("P", 0), a)] @{thm case_split}
 *}
 
 method_setup case_tac =