removed obsolete Sign.read_tyname/const (cf. ProofContext);
authorwenzelm
Wed Nov 07 16:42:55 2007 +0100 (2007-11-07)
changeset 2532350d4c8257d06
parent 25322 e2eac0c30ff5
child 25324 ed4ac5966c68
removed obsolete Sign.read_tyname/const (cf. ProofContext);
src/Pure/Isar/args.ML
src/Pure/sign.ML
     1.1 --- a/src/Pure/Isar/args.ML	Wed Nov 07 03:51:17 2007 +0100
     1.2 +++ b/src/Pure/Isar/args.ML	Wed Nov 07 16:42:55 2007 +0100
     1.3 @@ -330,10 +330,10 @@
     1.4  
     1.5  (* type and constant names *)
     1.6  
     1.7 -val tyname = Scan.peek (named_typ o Context.cases Sign.read_tyname ProofContext.read_tyname)
     1.8 +val tyname = Scan.peek (named_typ o ProofContext.read_tyname o Context.proof_of)
     1.9    >> (fn Type (c, _) => c | TFree (a, _) => a | _ => "");
    1.10  
    1.11 -val const = Scan.peek (named_term o Context.cases Sign.read_const ProofContext.read_const)
    1.12 +val const = Scan.peek (named_term o ProofContext.read_const o Context.proof_of)
    1.13    >> (fn Const (c, _) => c | Free (x, _) => x | _ => "");
    1.14  
    1.15  
     2.1 --- a/src/Pure/sign.ML	Wed Nov 07 03:51:17 2007 +0100
     2.2 +++ b/src/Pure/sign.ML	Wed Nov 07 16:42:55 2007 +0100
     2.3 @@ -142,8 +142,6 @@
     2.4    val read_typ: theory -> string -> typ
     2.5    val read_typ_syntax: theory -> string -> typ
     2.6    val read_typ_abbrev: theory -> string -> typ
     2.7 -  val read_tyname: theory -> string -> typ
     2.8 -  val read_const: theory -> string -> term
     2.9    val read_def_terms': Pretty.pp -> (string -> bool) -> Syntax.syntax -> Consts.T ->
    2.10      (string -> string option) -> Proof.context ->
    2.11      (indexname -> typ option) * (indexname -> sort option) ->
    2.12 @@ -524,16 +522,6 @@
    2.13  end;
    2.14  
    2.15  
    2.16 -(* type and constant names *)
    2.17 -
    2.18 -fun read_tyname thy raw_c =
    2.19 -  let val c = intern_type thy raw_c
    2.20 -  in Type (c, replicate (arity_number thy c) dummyT) end;
    2.21 -
    2.22 -val read_const = Consts.read_const o consts_of;
    2.23 -
    2.24 -
    2.25 -
    2.26  (* read_def_terms -- read terms and infer types *)    (*exception ERROR*)
    2.27  
    2.28  (*