tuned;
authorwenzelm
Mon Mar 13 13:16:43 2000 +0100 (2000-03-13)
changeset 8427b19b817522a5
parent 8426 f6e022588624
child 8428 be4c8a57cf7e
tuned;
src/Pure/Isar/rule_cases.ML
     1.1 --- a/src/Pure/Isar/rule_cases.ML	Mon Mar 13 13:16:26 2000 +0100
     1.2 +++ b/src/Pure/Isar/rule_cases.ML	Mon Mar 13 13:16:43 2000 +0100
     1.3 @@ -9,11 +9,12 @@
     1.4  sig
     1.5    type T (* = (string * typ) list * term list *)
     1.6    val name: string list -> thm -> thm
     1.7 +  val case_names: string list -> 'a attribute
     1.8    val get: thm -> string list
     1.9    val add: thm -> thm * string list
    1.10    val none: thm -> thm * string list
    1.11    val make: thm -> string list -> (string * T) list
    1.12 -  val case_names: string list -> 'a attribute
    1.13 +  val rename_params: string list list -> thm -> thm
    1.14    val params: string list list -> 'a attribute
    1.15  end;
    1.16  
    1.17 @@ -34,11 +35,9 @@
    1.18    |> Drule.untag_rule (casesN, [])
    1.19    |> Drule.tag_rule (casesN, names);
    1.20  
    1.21 -fun get thm =
    1.22 -  (case assoc (Thm.tags_of_thm thm, casesN) of
    1.23 -    None => map Library.string_of_int (1 upto Thm.nprems_of thm)
    1.24 -  | Some names => names);
    1.25 +fun case_names ss = Drule.rule_attribute (K (name ss));
    1.26  
    1.27 +fun get thm = Library.assocs (Thm.tags_of_thm thm) casesN;
    1.28  fun add thm = (thm, get thm);
    1.29  fun none thm = (thm, []);
    1.30  
    1.31 @@ -59,9 +58,7 @@
    1.32      (Library.drop (length names - Thm.nprems_of thm, names), ([], Thm.nprems_of thm)));
    1.33  
    1.34  
    1.35 -(* attributes *)
    1.36 -
    1.37 -fun case_names ss = Drule.rule_attribute (K (name ss));
    1.38 +(* params *)
    1.39  
    1.40  fun rename_params xss thm =
    1.41    #1 (foldl (fn ((th, i), xs) => (Thm.rename_params_rule (xs, i) th, i + 1)) ((thm, 1), xss));