# HG changeset patch
# User wenzelm
# Date 1194450175 -3600
# Node ID 50d4c8257d0668d60aacfae293e7f9a242e11ff8
# Parent  e2eac0c30ff5a7cb7a0ea81e84f369addd0473d4
removed obsolete Sign.read_tyname/const (cf. ProofContext);

diff -r e2eac0c30ff5 -r 50d4c8257d06 src/Pure/Isar/args.ML
--- a/src/Pure/Isar/args.ML	Wed Nov 07 03:51:17 2007 +0100
+++ b/src/Pure/Isar/args.ML	Wed Nov 07 16:42:55 2007 +0100
@@ -330,10 +330,10 @@
 
 (* type and constant names *)
 
-val tyname = Scan.peek (named_typ o Context.cases Sign.read_tyname ProofContext.read_tyname)
+val tyname = Scan.peek (named_typ o ProofContext.read_tyname o Context.proof_of)
   >> (fn Type (c, _) => c | TFree (a, _) => a | _ => "");
 
-val const = Scan.peek (named_term o Context.cases Sign.read_const ProofContext.read_const)
+val const = Scan.peek (named_term o ProofContext.read_const o Context.proof_of)
   >> (fn Const (c, _) => c | Free (x, _) => x | _ => "");
 
 
diff -r e2eac0c30ff5 -r 50d4c8257d06 src/Pure/sign.ML
--- 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*)
 
 (*