# HG changeset patch
# User wenzelm
# Date 1124356668 -7200
# Node ID 3b67c1809e1c3033bd78140232be1d3d4c88becb
# Parent  736f4b7841a83de707141de336f0e60dff716a89
added NO_CASES;

diff -r 736f4b7841a8 -r 3b67c1809e1c src/Pure/Isar/rule_cases.ML
--- 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;