src/Pure/Isar/rule_cases.ML

--- a/src/Pure/Isar/rule_cases.ML	Fri Jan 20 04:53:59 2006 +0100
+++ b/src/Pure/Isar/rule_cases.ML	Sat Jan 21 23:02:14 2006 +0100
@@ -33,15 +33,15 @@
   val consume: thm list -> thm list -> ('a * int) * thm ->
     (('a * (int * thm list)) * thm) Seq.seq
   val add_consumes: int -> thm -> thm
-  val consumes: int -> 'a attribute
-  val consumes_default: int -> 'a attribute
+  val consumes: int -> attribute
+  val consumes_default: int -> attribute
   val name: string list -> thm -> thm
-  val case_names: string list -> 'a attribute
-  val case_conclusion: string * string list -> 'a attribute
+  val case_names: string list -> attribute
+  val case_conclusion: string * string list -> attribute
   val save: thm -> thm -> thm
   val get: thm -> (string * string list) list * int
   val rename_params: string list list -> thm -> thm
-  val params: string list list -> 'a attribute
+  val params: string list list -> attribute
   val mutual_rule: thm list -> (int list * thm) option
   val strict_mutual_rule: thm list -> int list * thm
 end;
@@ -232,7 +232,7 @@
 
 val save_consumes = put_consumes o lookup_consumes;
 
-fun consumes n x = Drule.rule_attribute (K (put_consumes (SOME n))) x;
+fun consumes n x = Thm.rule_attribute (K (put_consumes (SOME n))) x;
 fun consumes_default n x =
   if Library.is_some (lookup_consumes (#2 x)) then x else consumes n x;
 
@@ -251,7 +251,7 @@
 
 val save_case_names = add_case_names o lookup_case_names;
 val name = add_case_names o SOME;
-fun case_names ss = Drule.rule_attribute (K (name ss));
+fun case_names ss = Thm.rule_attribute (K (name ss));
 
 
 
@@ -277,7 +277,7 @@
     | _ => NONE)
   in fold add_case_concl concls end;
 
-fun case_conclusion concl = Drule.rule_attribute (fn _ => add_case_concl concl);
+fun case_conclusion concl = Thm.rule_attribute (fn _ => add_case_concl concl);
 
 
 
@@ -304,7 +304,7 @@
   |> fold_index (fn (i, xs) => Thm.rename_params_rule (xs, i + 1)) xss
   |> save th;
 
-fun params xss = Drule.rule_attribute (K (rename_params xss));
+fun params xss = Thm.rule_attribute (K (rename_params xss));