# HG changeset patch
# User haftmann
# Date 1159822864 -7200
# Node ID a5343075bdc5d6c8e3f51c0253a525351168596e
# Parent  f5f69a1059f458623d66034b0e4b45f7b1496ce3
clarified some things

diff -r f5f69a1059f4 -r a5343075bdc5 src/Pure/Tools/class_package.ML
--- a/src/Pure/Tools/class_package.ML	Mon Oct 02 23:01:03 2006 +0200
+++ b/src/Pure/Tools/class_package.ML	Mon Oct 02 23:01:04 2006 +0200
@@ -50,8 +50,10 @@
   name_locale: string,
   name_axclass: string,
   var: string,
-  consts: (string * (string * typ)) list,
-    (*locale parameter ~> toplevel theory constant*)
+  consts: (string * (string * typ)) list
+    (*locale parameter ~> toplevel theory constant*),
+  operational: bool (* == at least one class operation,
+    or at least two operational superclasses *),
   propnames: string list
 } * thm list Symtab.table;
 
@@ -98,15 +100,10 @@
     of NONE => error ("undeclared constructive class " ^ quote class)
      | SOME data => data;
 
-fun is_operational_class thy cls =
-  lookup_class_data thy cls
-  |> Option.map (not o null o #consts o fst)
-  |> the_default false;
-
 fun the_ancestry thy classes =
   let
     fun proj_class class =
-      if is_operational_class thy class
+      if is_some (lookup_class_data thy class)
       then [class]
       else (Sign.certify_sort thy o maps proj_class o Sign.super_classes thy) class;
     fun ancestry class anc =
@@ -126,13 +123,14 @@
 
 (* updaters *)
 
-fun add_class_data (class, (name_locale, name_axclass, var, consts, propnames)) =
+fun add_class_data (class, (name_locale, name_axclass, var, consts, operational, propnames)) =
   ClassData.map (
     Symtab.update_new (class, ClassData ({
       name_locale = name_locale,
       name_axclass = name_axclass,
       var = var,
       consts = consts,
+      operational = operational,
       propnames = propnames}, Symtab.empty))
   );
 
@@ -316,6 +314,9 @@
       |> Sign.add_const_constraint_i (c, SOME (subst_clsvar v (TFree (v, [class])) ty));
     fun mk_const thy class v (c, ty) =
       Const (c, subst_clsvar v (TFree (v, [class])) ty);
+    fun is_operational thy mapp_this =
+      length mapp_this > 0 orelse
+        length (filter (#operational o fst o the o lookup_class_data thy) supclasses) > 1;
   in
     thy
     |> add_locale bname expr elems
@@ -329,8 +330,9 @@
           add_axclass_i (bname, supsort) (map (fst o snd) mapp_this) loc_axioms
     #-> (fn (name_axclass, (_, ax_axioms)) =>
           fold (add_global_constraint v name_axclass) mapp_this
-    #> add_class_data (name_locale, (name_locale, name_axclass, v, mapp_this,
-         map (fst o fst) loc_axioms))
+    #> `(fn thy => is_operational thy mapp_this)
+    #-> (fn operational => add_class_data (name_locale, (name_locale, name_axclass, v, mapp_this,
+          operational, map (fst o fst) loc_axioms)))
     #> prove_interpretation_i (bname, [])
           (Locale.Locale name_locale) (map (SOME o mk_const thy name_axclass v) (map snd (mapp_sup @ mapp_this)))
           ((ALLGOALS o ProofContext.fact_tac) ax_axioms)
@@ -530,6 +532,9 @@
 
 (** code generation view **)
 
+fun is_operational_class thy class =
+  the_default false ((Option.map (#operational o fst) o lookup_class_data thy) class);
+
 fun operational_algebra thy =
   Sorts.project_algebra (Sign.pp thy)
     (is_operational_class thy) (Sign.classes_of thy);