src/Pure/theory.ML

   in axioms' end);
 
 
 (* dependencies *)
 
-fun const_dep thy (c, T) = ((Defs.Constant, c), Sign.const_typargs thy (c, T));
+fun const_dep thy (c, T) = ((Defs.Const, c), Sign.const_typargs thy (c, T));
 fun type_dep (c, args) = ((Defs.Type, c), args);
 
 fun dependencies ctxt unchecked def description lhs rhs =
   let
     val thy = Proof_Context.theory_of ctxt;

       else error ("Specification depends on extra type variables: " ^
         commas_quote (map (Syntax.string_of_typ ctxt o TFree) rhs_extras) ^
         "\nThe error(s) above occurred in " ^ quote description);
   in Defs.define ctxt unchecked def description (prep lhs) (map prep rhs) end;
 
-fun cert_entry thy ((Defs.Constant, c), args) =
+fun cert_entry thy ((Defs.Const, c), args) =
       Sign.cert_term thy (Const (c, Sign.const_instance thy (c, args)))
       |> dest_Const |> const_dep thy
   | cert_entry thy ((Defs.Type, c), args) =
       Sign.certify_typ thy (Type (c, args)) |> dest_Type |> type_dep;