--- a/src/Pure/Isar/rule_cases.ML Thu Aug 18 11:17:47 2005 +0200
+++ b/src/Pure/Isar/rule_cases.ML Thu Aug 18 11:17:48 2005 +0200
@@ -19,6 +19,7 @@
val rename_params: string list list -> thm -> thm
val params: string list list -> 'a attribute
type tactic
+ val NO_CASES: Tactical.tactic -> tactic
end;
structure RuleCases: RULE_CASES =
@@ -144,4 +145,8 @@
type tactic = thm -> (thm * (string * T option) list) Seq.seq;
+fun NO_CASES tac = Seq.map (rpair []) o tac;
+
end;
+
+val NO_CASES = RuleCases.NO_CASES;