tuned;

--- a/src/Pure/defs.ML	Thu May 25 16:51:37 2006 +0200
+++ b/src/Pure/defs.ML	Thu May 25 16:51:39 2006 +0200
@@ -18,8 +18,8 @@
     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 =
@@ -191,11 +191,8 @@
 
 (* define *)
 
-fun define pp consts unchecked is_def module name lhs rhs (Defs defs) =
+fun define pp unchecked is_def module name (c, args) deps (Defs defs) =
   let
-    fun typargs const = (#1 const, Consts.typargs consts const);
-    val (c, args) = typargs lhs;
-    val deps = map typargs rhs;
     val restr =
       if plain_args args orelse
         (case args of [Type (a, rec_args)] => plain_args rec_args | _ => false)

--- a/src/Pure/theory.ML	Thu May 25 16:51:37 2006 +0200
+++ b/src/Pure/theory.ML	Thu May 25 16:51:39 2006 +0200
@@ -238,6 +238,9 @@
   let
     val pp = Sign.pp thy;
     val consts = Sign.consts_of thy;
+    fun prep const =
+      let val Const (c, T) = Sign.no_vars pp (Const const)
+      in (c, Consts.typargs consts (c, Compress.typ thy (Type.varifyT T))) end;
 
     val lhs_vars = Term.add_tfreesT (#2 lhs) [];
     val rhs_extras = fold (#2 #> Term.fold_atyps (fn TFree v =>
@@ -247,13 +250,7 @@
       else error ("Specification depends on extra type variables: " ^
         commas_quote (map (Pretty.string_of_typ pp o TFree) rhs_extras) ^
         "\nThe error(s) above occurred in " ^ quote name);
-
-    fun prep const =
-      let val Const (c, T) = Sign.no_vars pp (Const const)
-      in (c, Compress.typ thy (Type.varifyT T)) end;
-  in
-    Defs.define pp consts unchecked is_def (Context.theory_name thy) name (prep lhs) (map prep rhs)
-  end;
+  in Defs.define pp unchecked is_def (Context.theory_name thy) name (prep lhs) (map prep rhs) end;
 
 fun add_deps a raw_lhs raw_rhs thy =
   let