--- a/src/Pure/Isar/rule_cases.ML Mon Nov 12 23:27:04 2001 +0100
+++ b/src/Pure/Isar/rule_cases.ML Mon Nov 12 23:28:15 2001 +0100
@@ -16,6 +16,7 @@
val add: thm -> thm * (string list * int)
val save: thm -> thm -> thm
type T
+ val empty: T
val make: bool -> thm -> string list -> (string * T) list
val rename_params: string list list -> thm -> thm
val params: string list list -> 'a attribute
@@ -76,6 +77,8 @@
type T = {fixes: (string * typ) list, assumes: term list, binds: (indexname * term option) list};
+val empty = {fixes = [], assumes = [], binds = []};
+
fun prep_case open_parms thm name i =
let
val (_, _, Bi, _) = Thm.dest_state (thm, i)