src/FOL/cladata.ML

 
 (*Quantifier rules*)
 val FOL_cs = prop_cs addSIs [allI,ex_ex1I] addIs [exI] 
                      addSEs [exE,alt_ex1E] addEs [allE];
 
-val clasetup = [fn thy => (claset_ref_of thy := FOL_cs; thy)];
+val cla_setup = [fn thy => (claset_ref_of thy := FOL_cs; thy)];
+
+val case_setup =
+ [Method.add_methods
+    [("case_tac", Method.goal_args Args.name case_tac,
+      "case_tac emulation (dynamic instantiation!)")]];