--- a/src/Pure/sign.ML Wed Nov 07 03:51:17 2007 +0100
+++ b/src/Pure/sign.ML Wed Nov 07 16:42:55 2007 +0100
@@ -142,8 +142,6 @@
val read_typ: theory -> string -> typ
val read_typ_syntax: theory -> string -> typ
val read_typ_abbrev: theory -> string -> typ
- val read_tyname: theory -> string -> typ
- val read_const: theory -> string -> term
val read_def_terms': Pretty.pp -> (string -> bool) -> Syntax.syntax -> Consts.T ->
(string -> string option) -> Proof.context ->
(indexname -> typ option) * (indexname -> sort option) ->
@@ -524,16 +522,6 @@
end;
-(* type and constant names *)
-
-fun read_tyname thy raw_c =
- let val c = intern_type thy raw_c
- in Type (c, replicate (arity_number thy c) dummyT) end;
-
-val read_const = Consts.read_const o consts_of;
-
-
-
(* read_def_terms -- read terms and infer types *) (*exception ERROR*)
(*