--- a/src/FOL/cladata.ML Thu Jan 19 15:45:10 2006 +0100
+++ b/src/FOL/cladata.ML Thu Jan 19 21:22:08 2006 +0100
@@ -42,9 +42,9 @@
val FOL_cs = prop_cs addSIs [allI,ex_ex1I] addIs [exI]
addSEs [exE,alt_ex1E] addEs [allE];
-val cla_setup = [fn thy => (change_claset_of thy (fn _ => FOL_cs); thy)];
+val cla_setup = (fn thy => (change_claset_of thy (fn _ => FOL_cs); thy));
val case_setup =
- [Method.add_methods
+ (Method.add_methods
[("case_tac", Method.goal_args Args.name case_tac,
- "case_tac emulation (dynamic instantiation!)")]];
+ "case_tac emulation (dynamic instantiation!)")]);