# HG changeset patch
# User wenzelm
# Date 1176640316 -7200
# Node ID 92f8e9a8df78696110482bbf751fcf0b1625e292
# Parent  00fc658c4fe5afd28cf298b117b273dc107dc23c
removed obsolete inferT_axm;

diff -r 00fc658c4fe5 -r 92f8e9a8df78 src/Pure/theory.ML
--- a/src/Pure/theory.ML	Sun Apr 15 14:31:54 2007 +0200
+++ b/src/Pure/theory.ML	Sun Apr 15 14:31:56 2007 +0200
@@ -42,7 +42,6 @@
   val assert_super: theory -> theory -> theory
   val cert_axm: theory -> string * term -> string * term
   val read_axm: theory -> string * string -> string * term
-  val inferT_axm: theory -> string * term -> string * term
   val add_axioms: (bstring * string) list -> theory -> theory
   val add_axioms_i: (bstring * term) list -> theory -> theory
   val add_deps: string -> string * typ -> (string * typ) list -> theory -> theory
@@ -180,15 +179,6 @@
   cert_axm thy (name, Sign.read_prop thy str)
     handle ERROR msg => err_in_axm msg name;
 
-fun inferT_axm thy (name, pre_tm) =
-  let
-    val pp = Sign.pp thy;
-    val (t, _) =
-      Sign.infer_types pp thy (Sign.consts_of thy)
-        (K NONE) (K NONE) Name.context true ([pre_tm], propT);
-  in (name, Sign.no_vars pp t) end
-  handle ERROR msg => err_in_axm msg name;
-
 
 (* add_axioms(_i) *)