# HG changeset patch
# User wenzelm
# Date 957559024 -7200
# Node ID d04923e183c787a7cb922abee6c42057da2d81ca
# Parent  253dad743f00ab018d112121ff0e49a1c1817bb9
use Sign.simple_read_term;

diff -r 253dad743f00 -r d04923e183c7 src/ZF/Tools/datatype_package.ML
--- a/src/ZF/Tools/datatype_package.ML	Fri May 05 22:35:51 2000 +0200
+++ b/src/ZF/Tools/datatype_package.ML	Fri May 05 22:37:04 2000 +0200
@@ -412,13 +412,14 @@
 fun add_datatype (sdom, srec_tms, scon_ty_lists, 
 		  monos, type_intrs, type_elims) thy =
   let val sign = sign_of thy
-      val rec_tms = map (readtm sign Ind_Syntax.iT) srec_tms
+      val read_i = Sign.simple_read_term sign Ind_Syntax.iT
+      val rec_tms = map read_i srec_tms
       val con_ty_lists = Ind_Syntax.read_constructs sign scon_ty_lists
       val dom_sum = 
           if sdom = "" then
 	      Ind_Syntax.data_domain (#1(dest_Const Fp.oper) <> "Fixedpt.lfp") 
 	                             (rec_tms, con_ty_lists)
-          else readtm sign Ind_Syntax.iT sdom
+          else read_i sdom
   in 
       add_datatype_i (dom_sum, rec_tms, con_ty_lists, 
 		      monos, type_intrs, type_elims) thy
diff -r 253dad743f00 -r d04923e183c7 src/ZF/Tools/inductive_package.ML
--- a/src/ZF/Tools/inductive_package.ML	Fri May 05 22:35:51 2000 +0200
+++ b/src/ZF/Tools/inductive_package.ML	Fri May 05 22:37:04 2000 +0200
@@ -571,12 +571,14 @@
 (*external version, accepting strings*)
 fun add_inductive (srec_tms, sdom_sum, sintrs, monos,
 		     con_defs, type_intrs, type_elims) thy = 
-  let val rec_tms = map (readtm (sign_of thy) Ind_Syntax.iT) srec_tms
-      and dom_sum = readtm (sign_of thy) Ind_Syntax.iT sdom_sum
-      and intr_tms = map (readtm (sign_of thy) propT) sintrs
-  in  
-    add_inductive_i true (rec_tms, dom_sum, intr_tms, 
-			  monos, con_defs, type_intrs, type_elims) thy
+  let
+    val read = Sign.simple_read_term (Theory.sign_of thy);
+    val rec_tms = map (read Ind_Syntax.iT) srec_tms
+    and dom_sum = read Ind_Syntax.iT sdom_sum
+    and intr_tms = map (read propT) sintrs
+  in
+    thy
+    |> add_inductive_i true (rec_tms, dom_sum, intr_tms, monos, con_defs, type_intrs, type_elims)
+  end
 
-  end
 end;
diff -r 253dad743f00 -r d04923e183c7 src/ZF/Tools/primrec_package.ML
--- a/src/ZF/Tools/primrec_package.ML	Fri May 05 22:35:51 2000 +0200
+++ b/src/ZF/Tools/primrec_package.ML	Fri May 05 22:37:04 2000 +0200
@@ -191,6 +191,6 @@
   end;
 
 fun add_primrec eqns thy =
-  add_primrec_i (map (apsnd (readtm (sign_of thy) propT)) eqns) thy;
+  add_primrec_i (map (apsnd (Sign.simple_read_term (sign_of thy) propT)) eqns) thy;
 
 end;
diff -r 253dad743f00 -r d04923e183c7 src/ZF/ind_syntax.ML
--- a/src/ZF/ind_syntax.ML	Fri May 05 22:35:51 2000 +0200
+++ b/src/ZF/ind_syntax.ML	Fri May 05 22:37:04 2000 +0200
@@ -78,7 +78,7 @@
 
 (*read a constructor specification*)
 fun read_construct sign (id, sprems, syn) =
-    let val prems = map (readtm sign FOLogic.oT) sprems
+    let val prems = map (Sign.simple_read_term sign FOLogic.oT) sprems
         val args = map (#1 o dest_mem) prems
         val T = (map (#2 o dest_Free) args) ---> iT
                 handle TERM _ => error