# HG changeset patch
# User wenzelm
# Date 1194548882 -3600
# Node ID bf84dff3280dc55593095f9d0cbc898663a1b0dd
# Parent  a5fcf6d12a535d93129a430b3f7d7b417282d9fa
removed unused read_def_terms';

diff -r a5fcf6d12a53 -r bf84dff3280d 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