removed unused read_def_terms';
authorwenzelm
Thu, 08 Nov 2007 20:08:02 +0100
changeset 25351 bf84dff3280d
parent 25350 a5fcf6d12a53
child 25352 24d1568af397
removed unused read_def_terms';
src/Pure/sign.ML
--- 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