--- a/src/Tools/induct.ML Fri Mar 13 19:53:09 2009 +0100
+++ b/src/Tools/induct.ML Fri Mar 13 19:58:26 2009 +0100
@@ -738,20 +738,20 @@
fun cases_meth src =
Method.syntax (P.and_list' (Scan.repeat (unless_more_args inst)) -- Scan.option cases_rule) src
#> (fn ((insts, opt_rule), ctxt) =>
- Method.METHOD_CASES (fn facts =>
+ METHOD_CASES (fn facts =>
Seq.DETERM (HEADGOAL (cases_tac ctxt insts opt_rule facts))));
fun induct_meth src =
Method.syntax (P.and_list' (Scan.repeat (unless_more_args def_inst)) --
(arbitrary -- taking -- Scan.option induct_rule)) src
#> (fn ((insts, ((arbitrary, taking), opt_rule)), ctxt) =>
- Method.RAW_METHOD_CASES (fn facts =>
+ RAW_METHOD_CASES (fn facts =>
Seq.DETERM (HEADGOAL (induct_tac ctxt insts arbitrary taking opt_rule facts))));
fun coinduct_meth src =
Method.syntax (Scan.repeat (unless_more_args inst) -- taking -- Scan.option coinduct_rule) src
#> (fn (((insts, taking), opt_rule), ctxt) =>
- Method.RAW_METHOD_CASES (fn facts =>
+ RAW_METHOD_CASES (fn facts =>
Seq.DETERM (HEADGOAL (coinduct_tac ctxt insts taking opt_rule facts))));
end;