src/Pure/Isar/rule_cases.ML
changeset 18728 6790126ab5f6
parent 18608 9cdcc2a5c8b3
child 18799 f137c5e971f5
     1.1 --- a/src/Pure/Isar/rule_cases.ML	Fri Jan 20 04:53:59 2006 +0100
     1.2 +++ b/src/Pure/Isar/rule_cases.ML	Sat Jan 21 23:02:14 2006 +0100
     1.3 @@ -33,15 +33,15 @@
     1.4    val consume: thm list -> thm list -> ('a * int) * thm ->
     1.5      (('a * (int * thm list)) * thm) Seq.seq
     1.6    val add_consumes: int -> thm -> thm
     1.7 -  val consumes: int -> 'a attribute
     1.8 -  val consumes_default: int -> 'a attribute
     1.9 +  val consumes: int -> attribute
    1.10 +  val consumes_default: int -> attribute
    1.11    val name: string list -> thm -> thm
    1.12 -  val case_names: string list -> 'a attribute
    1.13 -  val case_conclusion: string * string list -> 'a attribute
    1.14 +  val case_names: string list -> attribute
    1.15 +  val case_conclusion: string * string list -> attribute
    1.16    val save: thm -> thm -> thm
    1.17    val get: thm -> (string * string list) list * int
    1.18    val rename_params: string list list -> thm -> thm
    1.19 -  val params: string list list -> 'a attribute
    1.20 +  val params: string list list -> attribute
    1.21    val mutual_rule: thm list -> (int list * thm) option
    1.22    val strict_mutual_rule: thm list -> int list * thm
    1.23  end;
    1.24 @@ -232,7 +232,7 @@
    1.25  
    1.26  val save_consumes = put_consumes o lookup_consumes;
    1.27  
    1.28 -fun consumes n x = Drule.rule_attribute (K (put_consumes (SOME n))) x;
    1.29 +fun consumes n x = Thm.rule_attribute (K (put_consumes (SOME n))) x;
    1.30  fun consumes_default n x =
    1.31    if Library.is_some (lookup_consumes (#2 x)) then x else consumes n x;
    1.32  
    1.33 @@ -251,7 +251,7 @@
    1.34  
    1.35  val save_case_names = add_case_names o lookup_case_names;
    1.36  val name = add_case_names o SOME;
    1.37 -fun case_names ss = Drule.rule_attribute (K (name ss));
    1.38 +fun case_names ss = Thm.rule_attribute (K (name ss));
    1.39  
    1.40  
    1.41  
    1.42 @@ -277,7 +277,7 @@
    1.43      | _ => NONE)
    1.44    in fold add_case_concl concls end;
    1.45  
    1.46 -fun case_conclusion concl = Drule.rule_attribute (fn _ => add_case_concl concl);
    1.47 +fun case_conclusion concl = Thm.rule_attribute (fn _ => add_case_concl concl);
    1.48  
    1.49  
    1.50  
    1.51 @@ -304,7 +304,7 @@
    1.52    |> fold_index (fn (i, xs) => Thm.rename_params_rule (xs, i + 1)) xss
    1.53    |> save th;
    1.54  
    1.55 -fun params xss = Drule.rule_attribute (K (rename_params xss));
    1.56 +fun params xss = Thm.rule_attribute (K (rename_params xss));
    1.57  
    1.58  
    1.59