added empty;
authorwenzelm
Mon Nov 12 23:28:15 2001 +0100 (2001-11-12 ago)
changeset 121665fc22b8c03e9
parent 12165 14e94ad99861
child 12167 74f92a43bac3
added empty;
src/Pure/Isar/rule_cases.ML
     1.1 --- a/src/Pure/Isar/rule_cases.ML	Mon Nov 12 23:27:04 2001 +0100
     1.2 +++ b/src/Pure/Isar/rule_cases.ML	Mon Nov 12 23:28:15 2001 +0100
     1.3 @@ -16,6 +16,7 @@
     1.4    val add: thm -> thm * (string list * int)
     1.5    val save: thm -> thm -> thm
     1.6    type T
     1.7 +  val empty: T
     1.8    val make: bool -> thm -> string list -> (string * T) list
     1.9    val rename_params: string list list -> thm -> thm
    1.10    val params: string list list -> 'a attribute
    1.11 @@ -76,6 +77,8 @@
    1.12  
    1.13  type T = {fixes: (string * typ) list, assumes: term list, binds: (indexname * term option) list};
    1.14  
    1.15 +val empty = {fixes = [], assumes = [], binds = []};
    1.16 +
    1.17  fun prep_case open_parms thm name i =
    1.18    let
    1.19      val (_, _, Bi, _) = Thm.dest_state (thm, i)