src/Pure/defs.ML
changeset 19727 f5895f998402
parent 19713 69c71d40f8a8
child 19729 cb9e2f0c7658
     1.1 --- a/src/Pure/defs.ML	Thu May 25 16:51:37 2006 +0200
     1.2 +++ b/src/Pure/defs.ML	Thu May 25 16:51:39 2006 +0200
     1.3 @@ -18,8 +18,8 @@
     1.4      reducts: ((string * typ list) * (string * typ list) list) list}
     1.5    val empty: T
     1.6    val merge: Pretty.pp -> T * T -> T
     1.7 -  val define: Pretty.pp -> Consts.T ->
     1.8 -    bool -> bool -> string -> string -> string * typ -> (string * typ) list -> T -> T
     1.9 +  val define: Pretty.pp -> bool -> bool -> string -> string ->
    1.10 +    string * typ list -> (string * typ list) list -> T -> T
    1.11  end
    1.12  
    1.13  structure Defs: DEFS =
    1.14 @@ -191,11 +191,8 @@
    1.15  
    1.16  (* define *)
    1.17  
    1.18 -fun define pp consts unchecked is_def module name lhs rhs (Defs defs) =
    1.19 +fun define pp unchecked is_def module name (c, args) deps (Defs defs) =
    1.20    let
    1.21 -    fun typargs const = (#1 const, Consts.typargs consts const);
    1.22 -    val (c, args) = typargs lhs;
    1.23 -    val deps = map typargs rhs;
    1.24      val restr =
    1.25        if plain_args args orelse
    1.26          (case args of [Type (a, rec_args)] => plain_args rec_args | _ => false)