misc tuning and clarification;

--- a/src/Pure/Isar/spec_rules.ML	Thu Nov 05 20:40:16 2009 +0100
+++ b/src/Pure/Isar/spec_rules.ML	Thu Nov 05 20:41:45 2009 +0100
@@ -1,18 +1,19 @@
 (*  Title:      Pure/Isar/spec_rules.ML
     Author:     Makarius
 
-Rules that characterize functional/relational specifications.  NB: In
-the face of arbitrary morphisms, the original shape of specifications
-may get transformed almost arbitrarily.
+Rules that characterize specifications, with rough classification.
+NB: In the face of arbitrary morphisms, the original shape of
+specifications may get lost.
 *)
 
 signature SPEC_RULES =
 sig
-  datatype kind = Functional | Relational | Co_Relational
-  val dest: Proof.context -> (kind * (term * thm list) list) list
-  val dest_global: theory -> (kind * (term * thm list) list) list
-  val add: kind * (term * thm list) list -> local_theory -> local_theory
-  val add_global: kind * (term * thm list) list -> theory -> theory
+  datatype rough_classification = Unknown | Equational | Inductive | Co_Inductive
+  type spec = rough_classification * (term list * thm list)
+  val get: Proof.context -> spec list
+  val get_global: theory -> spec list
+  val add: rough_classification -> term list * thm list -> local_theory -> local_theory
+  val add_global: rough_classification -> term list * thm list -> theory -> theory
 end;
 
 structure Spec_Rules: SPEC_RULES =
@@ -20,30 +21,34 @@
 
 (* maintain rules *)
 
-datatype kind = Functional | Relational | Co_Relational;
+datatype rough_classification = Unknown | Equational | Inductive | Co_Inductive;
+type spec = rough_classification * (term list * thm list);
 
 structure Rules = GenericDataFun
 (
-  type T = (kind * (term * thm list) list) Item_Net.T;
+  type T = spec Item_Net.T;
   val empty : T =
     Item_Net.init
-      (fn ((k1, spec1), (k2, spec2)) => k1 = k2 andalso
-        eq_list (fn ((t1, ths1), (t2, ths2)) =>
-          t1 aconv t2 andalso eq_list Thm.eq_thm_prop (ths1, ths2)) (spec1, spec2))
-      (map #1 o #2);
+      (fn ((class1, (ts1, ths1)), (class2, (ts2, ths2))) =>
+        class1 = class2 andalso
+        eq_list (op aconv) (ts1, ts2) andalso
+        eq_list Thm.eq_thm_prop (ths1, ths2))
+      (#1 o #2);
   val extend = I;
   fun merge _ = Item_Net.merge;
 );
 
-val dest = Item_Net.content o Rules.get o Context.Proof;
-val dest_global = Item_Net.content o Rules.get o Context.Theory;
+val get = Item_Net.content o Rules.get o Context.Proof;
+val get_global = Item_Net.content o Rules.get o Context.Theory;
 
-fun add (kind, specs) = LocalTheory.declaration
+fun add class (ts, ths) = LocalTheory.declaration
   (fn phi =>
-    let val specs' = map (fn (t, ths) => (Morphism.term phi t, Morphism.fact phi ths)) specs;
-    in Rules.map (Item_Net.update (kind, specs')) end);
+    let
+      val ts' = map (Morphism.term phi) ts;
+      val ths' = map (Morphism.thm phi) ths;
+    in Rules.map (Item_Net.update (class, (ts', ths'))) end);
 
-fun add_global entry =
-  Context.theory_map (Rules.map (Item_Net.update entry));
+fun add_global class spec =
+  Context.theory_map (Rules.map (Item_Net.update (class, spec)));
 
 end;