src/Pure/Isar/proof_context.ML
changeset 15703 727ef1b8b3ee
parent 15696 1da4ce092c0b
child 15725 95c33d627cdd
     1.1 --- a/src/Pure/Isar/proof_context.ML	Wed Apr 13 09:48:41 2005 +0200
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Wed Apr 13 18:34:22 2005 +0200
     1.3 @@ -8,7 +8,7 @@
     1.4  (*Jia: changed: datatype context
     1.5         affected files:  make_context, map_context, init, put_data, add_syntax, map_defaults, del_bind, upd_bind, qualified, hide_thms, put_thms, reset_thms, gen_assms, map_fixes, add_cases
     1.6  
     1.7 -       added: put_delta, get_delta 
     1.8 +       added: put_delta, get_delta
     1.9         06/01/05
    1.10  *)
    1.11  
    1.12 @@ -62,6 +62,8 @@
    1.13    val cert_prop_pats: context -> term list -> term list
    1.14    val declare_term: term -> context -> context
    1.15    val declare_terms: term list -> context -> context
    1.16 +  val read_tyname: context -> string -> typ
    1.17 +  val read_const: context -> string -> term
    1.18    val warn_extra_tfrees: context -> context -> context
    1.19    val generalize: context -> context -> term list -> term list
    1.20    val find_free: term -> string -> term option
    1.21 @@ -163,7 +165,7 @@
    1.22    val setup: (theory -> theory) list
    1.23  
    1.24    val get_delta: context -> Object.T Symtab.table (* Jia: (claset, simpset) *)
    1.25 -  val put_delta: Object.T Symtab.table -> context -> context 
    1.26 +  val put_delta: Object.T Symtab.table -> context -> context
    1.27    val get_delta_count_incr: context -> int
    1.28  
    1.29  end;
    1.30 @@ -648,10 +650,7 @@
    1.31  
    1.32  in
    1.33  
    1.34 -(* CB: for attribute where.  See attrib.ML. *)
    1.35  val read_termTs           = gen_read' (read_def_termTs false) (apfst o map) false false false;
    1.36 -
    1.37 -(* CB: for rule_tac etc.  See method.ML. *)
    1.38  val read_termTs_schematic = gen_read' (read_def_termTs false) (apfst o map) false false true;
    1.39  
    1.40  fun read_term_pats T ctxt =
    1.41 @@ -743,6 +742,19 @@
    1.42  end;
    1.43  
    1.44  
    1.45 +(* type and constant names *)
    1.46 +
    1.47 +fun read_tyname ctxt c =
    1.48 +  if c mem_string used_types ctxt then
    1.49 +    TFree (c, getOpt (def_sort ctxt (c, ~1), Sign.defaultS (sign_of ctxt)))
    1.50 +  else Sign.read_tyname (sign_of ctxt) c;
    1.51 +
    1.52 +fun read_const ctxt c =
    1.53 +  (case lookup_skolem ctxt c of
    1.54 +    SOME c' => Free (c', dummyT)
    1.55 +  | NONE => Sign.read_const (sign_of ctxt) c);
    1.56 +
    1.57 +
    1.58  
    1.59  (** Hindley-Milner polymorphism **)
    1.60