# HG changeset patch
# User nipkow
# Date 880386223 -3600
# Node ID 6c6073b13600592213b7eb2bf79996f9198b18da
# Parent  278660f52716f923800495ec2eccbe8a93d9f5cb
Added read_def_cterms for simultaneous reading/typing of terms under
defaults.
Redefined read_def_cterm in in terms of read_def_cterms.
Deleted obsolete read_cterms.

Cleaned up def of read_insts, which is not much shorter but much clearere are
correcter now.

diff -r 278660f52716 -r 6c6073b13600 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Sat Nov 22 13:27:02 1997 +0100
+++ b/src/Pure/drule.ML	Mon Nov 24 16:43:43 1997 +0100
@@ -123,7 +123,7 @@
    simultaneous instantiations were read or at least type checked
    simultaneously rather than one after the other. This would make the tricky
    composition of implicit type instantiations (parameter tye) superfluous.
-*)
+
 fun read_insts sign (rtypes,rsorts) (types,sorts) used insts =
 let val {tsig,...} = Sign.rep_sg sign
     fun split([],tvs,vs) = (tvs,vs)
@@ -152,6 +152,37 @@
 in (map (fn (ixn,T) => (ixn,ctyp_of sign T)) tye',
     map (fn (ixn,T,ct) => (cterm_of sign (Var(ixn,T)), ct)) cterms)
 end;
+*)
+
+fun read_insts sign (rtypes,rsorts) (types,sorts) used insts =
+let val {tsig,...} = Sign.rep_sg sign
+    fun split([],tvs,vs) = (tvs,vs)
+      | split((sv,st)::l,tvs,vs) = (case explode sv of
+                  "'"::cs => split(l,(indexname cs,st)::tvs,vs)
+                | cs => split(l,tvs,(indexname cs,st)::vs));
+    val (tvs,vs) = split(insts,[],[]);
+    fun readT((a,i),st) =
+        let val ixn = ("'" ^ a,i);
+            val S = case rsorts ixn of Some S => S | None => absent ixn;
+            val T = Sign.read_typ (sign,sorts) st;
+        in if Type.typ_instance(tsig,T,TVar(ixn,S)) then (ixn,T)
+           else inst_failure ixn
+        end
+    val tye = map readT tvs;
+    fun mkty(ixn,st) = (case rtypes ixn of
+                          Some T => (ixn,(st,typ_subst_TVars tye T))
+                        | None => absent ixn);
+    val ixnsTs = map mkty vs;
+    val ixns = map fst ixnsTs
+    and sTs  = map snd ixnsTs
+    val (cts,tye2) = read_def_cterms(sign,types,sorts) used false sTs;
+    fun mkcVar(ixn,T) =
+        let val U = typ_subst_TVars tye2 T
+        in cterm_of sign (Var(ixn,U)) end
+    val ixnTs = ListPair.zip(ixns, map snd sTs)
+in (map (fn (ixn,T) => (ixn,ctyp_of sign T)) (tye2 @ tye),
+    ListPair.zip(map mkcVar ixnTs,cts))
+end;
 
 
 (*** Find the type (sort) associated with a (T)Var or (T)Free in a term
diff -r 278660f52716 -r 6c6073b13600 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Sat Nov 22 13:27:02 1997 +0100
+++ b/src/Pure/thm.ML	Mon Nov 24 16:43:43 1997 +0100
@@ -24,7 +24,6 @@
   val cterm_of          : Sign.sg -> term -> cterm
   val ctyp_of_term      : cterm -> ctyp
   val read_cterm        : Sign.sg -> string * typ -> cterm
-  val read_cterms       : Sign.sg -> string list * typ list -> cterm list
   val cterm_fun         : (term -> term) -> (cterm -> cterm)
   val dest_comb         : cterm -> cterm * cterm
   val dest_abs          : cterm -> cterm * cterm
@@ -34,6 +33,10 @@
   val read_def_cterm    :
     Sign.sg * (indexname -> typ option) * (indexname -> sort option) ->
     string list -> bool -> string * typ -> cterm * (indexname * typ) list
+  val read_def_cterms   :
+    Sign.sg * (indexname -> typ option) * (indexname -> sort option) ->
+    string list -> bool -> (string * typ)list
+    -> cterm list * (indexname * typ)list
 
   (*proof terms [must DUPLICATE declaration as a specification]*)
   datatype deriv_kind = MinDeriv | ThmDeriv | FullDeriv;
@@ -258,23 +261,34 @@
 
 (** read cterms **)   (*exception ERROR*)
 
-(*read term, infer types, certify term*)
-fun read_def_cterm (sign, types, sorts) used freeze (a, T) =
+(*read terms, infer types, certify terms*)
+fun read_def_cterms (sign, types, sorts) used freeze sTs =
   let
-    val T' = Sign.certify_typ sign T
-      handle TYPE (msg, _, _) => error msg;
-    val ts = Syntax.read (#syn (Sign.rep_sg sign)) T' a;
-    val (t', tye) = Sign.infer_types sign types sorts used freeze (ts, T');
-    val ct = cterm_of sign t'
+    val syn = #syn (Sign.rep_sg sign)
+    fun read(s,T) =
+      let val T' = Sign.certify_typ sign T
+                   handle TYPE (msg, _, _) => error msg
+      in (Syntax.read syn T' s, T') end
+    val tsTs = map read sTs
+    val (ts',tye) = Sign.infer_types_simult sign types sorts used freeze tsTs;
+    val cts = map (cterm_of sign) ts'
       handle TYPE (msg, _, _) => error msg
            | TERM (msg, _) => error msg;
-  in (ct, tye) end;
+  in (cts, tye) end;
+
+(*read term, infer types, certify term*)
+fun read_def_cterm args used freeze aT =
+  let val ([ct],tye) = read_def_cterms args used freeze [aT]
+  in (ct,tye) end;
 
 fun read_cterm sign = #1 o read_def_cterm (sign, K None, K None) [] true;
 
 (*read a list of terms, matching them against a list of expected types.
   NO disambiguation of alternative parses via type-checking -- it is just
-  not practical.*)
+  not practical.
+
+Why not? In any case, this function is not used at all.
+
 fun read_cterms sg (bs, Ts) =
   let
     val {tsig, syn, ...} = Sign.rep_sg sg;
@@ -293,7 +307,7 @@
   in map (cterm_of sg) us end
   handle TYPE (msg, _, _) => error msg
        | TERM (msg, _) => error msg;
-
+*)
 
 
 (*** Derivations ***)