src/Pure/sign.ML
changeset 25351 bf84dff3280d
parent 25323 50d4c8257d06
child 25366 05c2ae18cc51
--- a/src/Pure/sign.ML	Thu Nov 08 20:08:01 2007 +0100
+++ b/src/Pure/sign.ML	Thu Nov 08 20:08:02 2007 +0100
@@ -142,10 +142,6 @@
   val read_typ: theory -> string -> typ
   val read_typ_syntax: theory -> string -> typ
   val read_typ_abbrev: theory -> string -> typ
-  val read_def_terms': Pretty.pp -> (string -> bool) -> Syntax.syntax -> Consts.T ->
-    (string -> string option) -> Proof.context ->
-    (indexname -> typ option) * (indexname -> sort option) ->
-    Name.context -> bool -> (string * typ) list -> term list * (indexname * typ) list
   val read_def_terms:
     theory * (indexname -> typ option) * (indexname -> sort option) ->
     string list -> bool -> (string * typ) list -> term list * (indexname * typ) list