removed obsolete inferT_axm;
authorwenzelm
Sun Apr 15 14:31:56 2007 +0200 (2007-04-15)
changeset 2269792f8e9a8df78
parent 22696 00fc658c4fe5
child 22698 7e6412e8d64b
removed obsolete inferT_axm;
src/Pure/theory.ML
     1.1 --- a/src/Pure/theory.ML	Sun Apr 15 14:31:54 2007 +0200
     1.2 +++ b/src/Pure/theory.ML	Sun Apr 15 14:31:56 2007 +0200
     1.3 @@ -42,7 +42,6 @@
     1.4    val assert_super: theory -> theory -> theory
     1.5    val cert_axm: theory -> string * term -> string * term
     1.6    val read_axm: theory -> string * string -> string * term
     1.7 -  val inferT_axm: theory -> string * term -> string * term
     1.8    val add_axioms: (bstring * string) list -> theory -> theory
     1.9    val add_axioms_i: (bstring * term) list -> theory -> theory
    1.10    val add_deps: string -> string * typ -> (string * typ) list -> theory -> theory
    1.11 @@ -180,15 +179,6 @@
    1.12    cert_axm thy (name, Sign.read_prop thy str)
    1.13      handle ERROR msg => err_in_axm msg name;
    1.14  
    1.15 -fun inferT_axm thy (name, pre_tm) =
    1.16 -  let
    1.17 -    val pp = Sign.pp thy;
    1.18 -    val (t, _) =
    1.19 -      Sign.infer_types pp thy (Sign.consts_of thy)
    1.20 -        (K NONE) (K NONE) Name.context true ([pre_tm], propT);
    1.21 -  in (name, Sign.no_vars pp t) end
    1.22 -  handle ERROR msg => err_in_axm msg name;
    1.23 -
    1.24  
    1.25  (* add_axioms(_i) *)
    1.26