# HG changeset patch
# User wenzelm
# Date 898365185 -7200
# Node ID 16e3fadd759ec13a6dcf340861939b4a184a290e
# Parent  e88cc76cb052c1e221a526c639454b5698876058
added read_def_axm;

diff -r e88cc76cb052 -r 16e3fadd759e src/Pure/theory.ML
--- a/src/Pure/theory.ML	Sat Jun 20 19:52:53 1998 +0200
+++ b/src/Pure/theory.ML	Sat Jun 20 19:53:05 1998 +0200
@@ -24,6 +24,8 @@
   val subthy: theory * theory -> bool
   val eq_thy: theory * theory -> bool
   val cert_axm: Sign.sg -> string * term -> string * term
+  val read_def_axm: Sign.sg * (indexname -> typ option) * (indexname -> sort option) -> string list ->
+    string * string -> string * term
   val read_axm: Sign.sg -> string * string -> string * term
   val inferT_axm: Sign.sg -> string * term -> string * term
   val merge_theories: string -> theory * theory -> theory
@@ -228,14 +230,16 @@
   end
   handle ERROR => err_in_axm name;
 
-(*Some duplication of code with read_def_cterm*)
-fun read_axm sg (name, str) = 
+(*some duplication of code with read_def_cterm*)
+fun read_def_axm (sg, types, sorts) used (name, str) = 
   let
     val ts = Syntax.read (#syn (Sign.rep_sg sg)) propT str;
-    val (t, _) = Sign.infer_types sg (K None) (K None) [] true (ts, propT);
+    val (t, _) = Sign.infer_types sg types sorts used true (ts, propT);
   in cert_axm sg (name,t) end
   handle ERROR => err_in_axm name;
 
+fun read_axm sg name_str = read_def_axm (sg, K None, K None) [] name_str;
+
 fun inferT_axm sg (name, pre_tm) =
   let
     val (t, _) = Sign.infer_types sg (K None) (K None) [] true ([pre_tm], propT);