src/Pure/theory.ML

 
 fun dependencies ctxt unchecked def description lhs rhs =
   let
     val thy = Proof_Context.theory_of ctxt;
     val consts = Sign.consts_of thy;
+
     fun prep (DConst const) =
-      let val Const (c, T) = Sign.no_vars ctxt (Const const)
-      in (Defs.NConst c, Consts.typargs consts (c, Logic.varifyT_global T)) end
+        let val Const (c, T) = Sign.no_vars ctxt (Const const)
+        in ((Defs.Constant, c), Consts.typargs consts (c, Logic.varifyT_global T)) end
     | prep (DType typ) =
-      let val Type (c, T) = Type.no_tvars (Type typ)
-      in (Defs.NType c, map Logic.varifyT_global T) end;
+        let val Type (c, Ts) = Type.no_tvars (Type typ)
+        in ((Defs.Type, c), map Logic.varifyT_global Ts) end;
+
     fun fold_dep_tfree f (DConst (_, T)) = fold_atyps (fn TFree v => f v | _ => I) T
-      | fold_dep_tfree f (DType (_, Ts)) = fold (fold_atyps (fn TFree v => f v | _ => I)) Ts
+      | fold_dep_tfree f (DType (_, Ts)) = fold (fold_atyps (fn TFree v => f v | _ => I)) Ts;
+
     val lhs_vars = fold_dep_tfree (insert (op =)) lhs [];
     val rhs_extras = fold (fold_dep_tfree
       (fn v => if member (op =) lhs_vars v then I else insert (op =) v)) rhs [];
     val _ =
       if null rhs_extras then ()