# HG changeset patch
# User wenzelm
# Date 1210967609 -7200
# Node ID 54dce7c7c76f4eb6d15e98763a7d44e904e84232
# Parent  c795d4b706b1a3bc6fcb5013b671762c8e92c9b3
removed unused make_simple;

diff -r c795d4b706b1 -r 54dce7c7c76f src/Pure/Isar/rule_cases.ML
--- a/src/Pure/Isar/rule_cases.ML	Fri May 16 21:53:27 2008 +0200
+++ b/src/Pure/Isar/rule_cases.ML	Fri May 16 21:53:29 2008 +0200
@@ -28,7 +28,6 @@
   val strip_params: term -> (string * typ) list
   val make_common: bool -> theory * term -> (string * string list) list -> cases
   val make_nested: bool -> term -> theory * term -> (string * string list) list -> cases
-  val make_simple: bool -> theory * term -> string -> cases
   val apply: term list -> T -> T
   val consume: thm list -> thm list -> ('a * int) * thm ->
     (('a * (int * thm list)) * thm) Seq.seq
@@ -150,7 +149,6 @@
 
 fun make_common is_open = make is_open NONE;
 fun make_nested is_open rule_struct = make is_open (SOME rule_struct);
-fun make_simple is_open (thy, prop) name = [(name, extract_case is_open thy (NONE, prop) "" [])];
 
 fun apply args =
   let