added read_def_axm;
authorwenzelm
Sat Jun 20 19:53:05 1998 +0200 (1998-06-20)
changeset 505716e3fadd759e
parent 5056 e88cc76cb052
child 5058 52a78ff5599e
added read_def_axm;
src/Pure/theory.ML
     1.1 --- a/src/Pure/theory.ML	Sat Jun 20 19:52:53 1998 +0200
     1.2 +++ b/src/Pure/theory.ML	Sat Jun 20 19:53:05 1998 +0200
     1.3 @@ -24,6 +24,8 @@
     1.4    val subthy: theory * theory -> bool
     1.5    val eq_thy: theory * theory -> bool
     1.6    val cert_axm: Sign.sg -> string * term -> string * term
     1.7 +  val read_def_axm: Sign.sg * (indexname -> typ option) * (indexname -> sort option) -> string list ->
     1.8 +    string * string -> string * term
     1.9    val read_axm: Sign.sg -> string * string -> string * term
    1.10    val inferT_axm: Sign.sg -> string * term -> string * term
    1.11    val merge_theories: string -> theory * theory -> theory
    1.12 @@ -228,14 +230,16 @@
    1.13    end
    1.14    handle ERROR => err_in_axm name;
    1.15  
    1.16 -(*Some duplication of code with read_def_cterm*)
    1.17 -fun read_axm sg (name, str) = 
    1.18 +(*some duplication of code with read_def_cterm*)
    1.19 +fun read_def_axm (sg, types, sorts) used (name, str) = 
    1.20    let
    1.21      val ts = Syntax.read (#syn (Sign.rep_sg sg)) propT str;
    1.22 -    val (t, _) = Sign.infer_types sg (K None) (K None) [] true (ts, propT);
    1.23 +    val (t, _) = Sign.infer_types sg types sorts used true (ts, propT);
    1.24    in cert_axm sg (name,t) end
    1.25    handle ERROR => err_in_axm name;
    1.26  
    1.27 +fun read_axm sg name_str = read_def_axm (sg, K None, K None) [] name_str;
    1.28 +
    1.29  fun inferT_axm sg (name, pre_tm) =
    1.30    let
    1.31      val (t, _) = Sign.infer_types sg (K None) (K None) [] true ([pre_tm], propT);