# HG changeset patch
# User wenzelm
# Date 777303699 -7200
# Node ID eec3a9222b50e50fb9be91b462c43c86031e3f5a
# Parent  e9bf62651beb74621c1c039b186be152a0dff17d
added inferT_axm;
removed extend_theory;
changed read_def_cterm: now uses Sign.infer_types;

diff -r e9bf62651beb -r eec3a9222b50 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Fri Aug 19 15:41:00 1994 +0200
+++ b/src/Pure/thm.ML	Fri Aug 19 15:41:39 1994 +0200
@@ -31,10 +31,8 @@
   val typ_of: ctyp -> typ
   val cterm_fun: (term -> term) -> (cterm -> cterm)
   (*end of cterm/ctyp functions*)
-
-  (* FIXME *)
-  local open Sign.Syntax Sign.Syntax.Mixfix in  (* FIXME remove ...Mixfix *)
-    val add_classes: (class list * class * class list) list -> theory -> theory
+  local open Sign.Syntax in
+    val add_classes: (class * class list) list -> theory -> theory
     val add_classrel: (class * class) list -> theory -> theory
     val add_defsort: sort -> theory -> theory
     val add_types: (string * int * mixfix) list -> theory -> theory
@@ -59,6 +57,7 @@
   end
   val cert_axm: Sign.sg -> string * term -> string * term
   val read_axm: Sign.sg -> string * string -> string * term
+  val inferT_axm: Sign.sg -> string * term -> string * term
   val abstract_rule: string -> cterm -> thm -> thm
   val add_congs: meta_simpset * thm list -> meta_simpset
   val add_prems: meta_simpset * thm list -> meta_simpset
@@ -79,13 +78,6 @@
   val eq_assumption: int -> thm -> thm
   val equal_intr: thm -> thm -> thm
   val equal_elim: thm -> thm -> thm
-  val extend_theory: theory -> string
-        -> (class * class list) list * sort
-           * (string list * int)list
-           * (string * string list * string) list
-           * (string list * (sort list * class))list
-           * (string list * string)list * Sign.Syntax.sext option
-        -> (string*string)list -> theory
   val extensional: thm -> thm
   val flexflex_rule: thm -> thm Sequence.seq
   val flexpair_def: thm
@@ -193,26 +185,13 @@
 
 
 
-(** read cterms **)
+(** read cterms **)   (*exception ERROR*)     (* FIXME check *)
 
 (*read term, infer types, certify term*)
-
 fun read_def_cterm (sign, types, sorts) (a, T) =
   let
-    val {tsig, const_tab, syn, ...} = Sign.rep_sg sign;
-    val showtyp = Sign.string_of_typ sign;
-    val showterm = Sign.string_of_term sign;
-
-    fun termerr [] = ""
-      | termerr [t] = "\nInvolving this term:\n" ^ showterm t
-      | termerr ts = "\nInvolving these terms:\n" ^ cat_lines (map showterm ts);
-
-    val T' = Sign.certify_typ sign T
-      handle TYPE (msg, _, _) => error msg;
-    val t = Syntax.read syn T' a;
-    val (t', tye) = Type.infer_types (tsig, const_tab, types, sorts, T', t)
-      handle TYPE (msg, Ts, ts) => error ("Type checking error: " ^ msg ^ "\n"
-        ^ cat_lines (map showtyp Ts) ^ termerr ts);
+    val t = Syntax.read (#syn (Sign.rep_sg sign)) T a;
+    val (t', tye) = Sign.infer_types sign types sorts (t, T);
     val ct = cterm_of sign t' handle TERM (msg, _) => error msg;
   in (ct, tye) end;
 
@@ -375,6 +354,10 @@
   (name, no_vars (term_of (read_cterm sg (str, propT))))
     handle ERROR => err_in_axm name;
 
+fun inferT_axm sg (name, pre_tm) =
+  (name, no_vars (#1 (Sign.infer_types sg (K None) (K None) (pre_tm, propT))))
+    handle ERROR => err_in_axm name;
+
 
 (* extend axioms of a theory *)
 
@@ -390,30 +373,6 @@
 val add_axioms_i = ext_axms cert_axm;
 
 
-(* extend theory (old) *)   (* FIXME remove *)
-
-(*converts Frees to Vars: axioms can be written without question marks*)
-fun prepare_axiom sign sP =
-  Logic.varify (term_of (read_cterm sign (sP, propT)));
-
-(*read an axiom for a new theory*)
-fun read_ax sign (a, sP) =
-  (a, prepare_axiom sign sP) handle ERROR => err_in_axm a;
-
-(*extension of a theory with given classes, types, constants and syntax;
-  reads the axioms from strings: axpairs have the form (axname, axiom)*)
-fun extend_theory thy thyname ext axpairs =
-  let
-    val Theory {sign, ...} = thy;
-
-    val sign1 = Sign.extend sign thyname ext;
-    val axioms = map (read_ax sign1) axpairs;
-  in
-    writeln "WARNING: called obsolete function \"extend_theory\"";
-    ext_thy thy sign1 axioms
-  end;
-
-
 
 (** merge theories **)