# HG changeset patch
# User ballarin
# Date 1071062984 -3600
# Node ID f630017ed01c902b7d3b0a2008653e5d50f9b9c5
# Parent  0ae66ffb978421313bdcb5dcde8fdae52f54e46c
Isar: where attribute supports instantiation of type variables.

diff -r 0ae66ffb9784 -r f630017ed01c src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Wed Dec 10 14:29:05 2003 +0100
+++ b/src/Pure/Isar/attrib.ML	Wed Dec 10 14:29:44 2003 +0100
@@ -196,6 +196,7 @@
 
 
 (* where: named instantiations *)
+(*        permits instantiation of type and term variables *)
 
 fun read_instantiate _ [] _ thm = thm
   | read_instantiate context_of insts x thm =
@@ -203,19 +204,52 @@
         val ctxt = context_of x;
         val sign = ProofContext.sign_of ctxt;
 
-        val vars = Drule.vars_of thm;
+        (* Separate type and term insts,
+           type insts must occur strictly before term insts *)
+        fun has_type_var ((x, _), _) = (case Symbol.explode x of
+             "'"::cs => true | cs => false);
+        val (Tinst, tinsts) = take_prefix has_type_var insts;
+	val _ = if exists has_type_var tinsts
+              then error
+                "Type instantiations must occur before term instantiations."
+              else ();
+
+        val Tinsts = filter has_type_var insts;
+        val tinsts = filter_out has_type_var insts;
+
+        (* Type instantiations first *)
+	(* Process type insts: Tinsts_env *)
+	fun absent xi = error
+	      ("No such type variable in theorem: " ^
+               Syntax.string_of_vname xi);
+	val (rtypes, rsorts) = types_sorts thm;
+	fun readT (xi, s) =
+	    let val S = case rsorts xi of Some S => S | None => absent xi;
+		val T = ProofContext.read_typ ctxt s;
+	    in if Sign.typ_instance sign (T, TVar (xi, S)) then (xi, T)
+	       else error
+		 ("Instantiation of " ^ Syntax.string_of_vname xi ^ " fails")
+	    end;
+	val Tinsts_env = map readT Tinsts;
+	val cenvT = map (apsnd (Thm.ctyp_of sign)) (Tinsts_env);
+        val thm' = Thm.instantiate (cenvT, []) thm;
+           (* Instantiate, but don't normalise: *)
+           (* this happens after term insts anyway. *)
+
+        (* Term instantiations *)
+        val vars = Drule.vars_of thm';
         fun get_typ xi =
           (case assoc (vars, xi) of
             Some T => T
           | None => error ("No such variable in theorem: " ^ Syntax.string_of_vname xi));
 
-        val (xs, ss) = Library.split_list insts;
+        val (xs, ss) = Library.split_list tinsts;
         val Ts = map get_typ xs;
 
-        val used = add_term_tvarnames (prop_of thm,[])
-        (* Names of TVars occuring in thm.  read_termTs ensures
+        val used = add_term_tvarnames (prop_of thm',[])
+        (* Names of TVars occuring in thm'.  read_termTs ensures
            that new TVars introduced when reading the instantiation string
-           are distinct from used ones. *)
+           are distinct from those occuring in the theorem. *)
 
         val (ts, envT) = ProofContext.read_termTs used ctxt (ss ~~ Ts);
         val cenvT = map (apsnd (Thm.ctyp_of sign)) envT;
@@ -223,7 +257,7 @@
           map (fn (xi, t) => pairself (Thm.cterm_of sign) (Var (xi, fastype_of t), t))
             (gen_distinct (fn ((x1, t1), (x2, t2)) => x1 = x2 andalso t1 aconv t2) (xs ~~ ts));
       in
-        thm
+        thm'
         |> Drule.instantiate (cenvT, cenv)
         |> RuleCases.save thm
       end;
@@ -237,6 +271,7 @@
 
 
 (* of: positional instantiations *)
+(*        permits instantiation of term variables only *)
 
 fun read_instantiate' _ ([], []) _ thm = thm
   | read_instantiate' context_of (args, concl_args) x thm =
diff -r 0ae66ffb9784 -r f630017ed01c src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Wed Dec 10 14:29:05 2003 +0100
+++ b/src/Pure/Isar/proof_context.ML	Wed Dec 10 14:29:44 2003 +0100
@@ -421,6 +421,8 @@
 
 in
 
+(* Read/certify type, using default sort information from context. *)
+
 val read_typ = read_typ_aux Sign.read_typ';
 val read_typ_no_norm = read_typ_aux Sign.read_typ_no_norm';
 val cert_typ = cert_typ_aux Sign.certify_typ;