diff -r bc51b343f80d -r 983dfcce45ad src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Wed Apr 15 15:34:54 2009 +0200
+++ b/src/Pure/Isar/code.ML	Wed Apr 15 15:38:30 2009 +0200
@@ -29,8 +29,6 @@
   val add_undefined: string -> theory -> theory
   val purge_data: theory -> theory
 
-  val coregular_algebra: theory -> Sorts.algebra
-  val operational_algebra: theory -> (sort -> sort) * Sorts.algebra
   val these_eqns: theory -> string -> (thm * bool) list
   val these_raw_eqns: theory -> string -> (thm * bool) list
   val get_datatype: theory -> string -> ((string * sort) list * (string * typ list) list)
@@ -469,39 +467,6 @@
 fun mk_default_eqn thy = Code_Unit.try_thm (check_linear o Code_Unit.mk_eqn thy);
 
 
-(** operational sort algebra and class discipline **)
-
-local
-
-fun arity_constraints thy algebra (class, tyco) =
-  let
-    val base_constraints = Sorts.mg_domain algebra tyco [class];
-    val classparam_constraints = Sorts.complete_sort algebra [class]
-      |> maps (map fst o these o try (#params o AxClass.get_info thy))
-      |> map_filter (fn c => try (AxClass.param_of_inst thy) (c, tyco))
-      |> maps (map fst o get_eqns thy)
-      |> map (map (snd o dest_TVar) o Sign.const_typargs thy o Code_Unit.const_typ_eqn);
-    val inter_sorts = map2 (curry (Sorts.inter_sort algebra));
-  in fold inter_sorts classparam_constraints base_constraints end;
-
-fun retrieve_algebra thy operational =
-  Sorts.subalgebra (Syntax.pp_global thy) operational
-    (SOME o arity_constraints thy (Sign.classes_of thy))
-    (Sign.classes_of thy);
-
-in
-
-fun coregular_algebra thy = retrieve_algebra thy (K true) |> snd;
-fun operational_algebra thy =
-  let
-    fun add_iff_operational class =
-      can (AxClass.get_info thy) class ? cons class;
-    val operational_classes = fold add_iff_operational (Sign.all_classes thy) []
-  in retrieve_algebra thy (member (op =) operational_classes) end;
-
-end; (*local*)
-
-
 (** interfaces and attributes **)
 
 fun delete_force msg key xs =