src/Pure/defs.ML

   val dest: T ->
    {restricts: ((string * typ list) * string) list,
     reducts: ((string * typ list) * (string * typ list) list) list}
   val empty: T
   val merge: Pretty.pp -> T * T -> T
-  val define: Pretty.pp -> Consts.T ->
-    bool -> bool -> string -> string -> string * typ -> (string * typ) list -> T -> T
+  val define: Pretty.pp -> bool -> bool -> string -> string ->
+    string * typ list -> (string * typ list) list -> T -> T
 end
 
 structure Defs: DEFS =
 struct
 

   in Defs (Symtab.join join_specs (defs1, defs2) |> Symtab.fold add_def defs2) end;
 
 
 (* define *)
 
-fun define pp consts unchecked is_def module name lhs rhs (Defs defs) =
-  let
-    fun typargs const = (#1 const, Consts.typargs consts const);
-    val (c, args) = typargs lhs;
-    val deps = map typargs rhs;
+fun define pp unchecked is_def module name (c, args) deps (Defs defs) =
+  let
     val restr =
       if plain_args args orelse
         (case args of [Type (a, rec_args)] => plain_args rec_args | _ => false)
       then [] else [(args, name)];
     val spec =