# HG changeset patch
# User berghofe
# Date 1106055264 -3600
# Node ID 3b75e1b22ff1e87428a8f8d496cce5eed3f748e3
# Parent  42b858b978b833bd17fd1e95daefbe5b835469dc
Added variants of instantiation functions that operate on pairs of type
(indexname * string) instead of (string * string).

diff -r 42b858b978b8 -r 3b75e1b22ff1 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Mon Jan 17 17:45:03 2005 +0100
+++ b/src/Pure/drule.ML	Tue Jan 18 14:34:24 2005 +0100
@@ -20,7 +20,7 @@
   val read_insts        :
           Sign.sg -> (indexname -> typ option) * (indexname -> sort option)
                   -> (indexname -> typ option) * (indexname -> sort option)
-                  -> string list -> (string*string)list
+                  -> string list -> (indexname * string) list
                   -> (indexname*ctyp)list * (cterm*cterm)list
   val types_sorts: thm -> (indexname-> typ option) * (indexname-> sort option)
   val strip_shyps_warning : thm -> thm
@@ -218,14 +218,11 @@
 
 fun read_insts sign (rtypes,rsorts) (types,sorts) used insts =
 let
-    fun split([],tvs,vs) = (tvs,vs)
-      | split((sv,st)::l,tvs,vs) = (case Symbol.explode sv of
-                  "'"::cs => split(l,(Syntax.indexname cs,st)::tvs,vs)
-                | cs => split(l,tvs,(Syntax.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;
+    fun is_tv ((a, _), _) =
+      (case Symbol.explode a of "'" :: _ => true | _ => false);
+    val (tvs, vs) = partition is_tv insts;
+    fun readT (ixn, st) =
+        let val S = case rsorts ixn of Some S => S | None => absent ixn;
             val T = Sign.read_typ (sign,sorts) st;
         in if Sign.typ_instance sign (T, TVar(ixn,S)) then (ixn,T)
            else inst_failure ixn
@@ -789,7 +786,8 @@
 fun read_instantiate_sg sg sinsts th =
     let val ts = types_sorts th;
         val used = add_term_tvarnames (prop_of th, []);
-    in  instantiate (read_insts sg ts ts used sinsts) th  end;
+        val sinsts' = map (apfst Syntax.indexname) sinsts
+    in  instantiate (read_insts sg ts ts used sinsts') th  end;
 
 (*Instantiate theorem th, reading instantiations under theory of th*)
 fun read_instantiate sinsts th =
diff -r 42b858b978b8 -r 3b75e1b22ff1 src/Pure/tactic.ML
--- a/src/Pure/tactic.ML	Mon Jan 17 17:45:03 2005 +0100
+++ b/src/Pure/tactic.ML	Tue Jan 18 14:34:24 2005 +0100
@@ -111,6 +111,10 @@
   val conjunction_tac: tactic
   val prove: Sign.sg -> string list -> term list -> term -> (thm list -> tactic) -> thm
   val prove_standard: Sign.sg -> string list -> term list -> term -> (thm list -> tactic) -> thm
+  val compose_inst_tac' : (indexname * string) list -> (bool * thm * int) ->
+                          int -> tactic
+  val lift_inst_rule'   : thm * int * (indexname * string) list * thm -> thm
+  val res_inst_tac'     : (indexname * string) list -> thm -> int -> tactic
 end;
 
 structure Tactic: TACTIC =
@@ -212,7 +216,7 @@
   in rename_wrt_term Bi (Logic.strip_params Bi) end;
 
 (*Lift and instantiate a rule wrt the given state and subgoal number *)
-fun lift_inst_rule (st, i, sinsts, rule) =
+fun lift_inst_rule' (st, i, sinsts, rule) =
 let val {maxidx,sign,...} = rep_thm st
     val (_, _, Bi, _) = dest_state(st,i)
     val params = Logic.strip_params Bi          (*params of subgoal i*)
@@ -238,6 +242,9 @@
                      (lift_rule (st,i) rule)
 end;
 
+fun lift_inst_rule (st, i, sinsts, rule) = lift_inst_rule'
+  (st, i, map (apfst Syntax.indexname) sinsts, rule);
+
 (*
 Like lift_inst_rule but takes terms, not strings, where the terms may contain
 Bounds referring to parameters of the subgoal.
@@ -271,13 +278,16 @@
      subgoal.  Fails if "i" is out of range.  ***)
 
 (*compose version: arguments are as for bicompose.*)
-fun compose_inst_tac sinsts (bires_flg, rule, nsubgoal) i st =
+fun gen_compose_inst_tac instf sinsts (bires_flg, rule, nsubgoal) i st =
   if i > nprems_of st then no_tac st
   else st |>
-    (compose_tac (bires_flg, lift_inst_rule (st, i, sinsts, rule), nsubgoal) i
+    (compose_tac (bires_flg, instf (st, i, sinsts, rule), nsubgoal) i
      handle TERM (msg,_)   => (warning msg;  no_tac)
           | THM  (msg,_,_) => (warning msg;  no_tac));
 
+val compose_inst_tac = gen_compose_inst_tac lift_inst_rule;
+val compose_inst_tac' = gen_compose_inst_tac lift_inst_rule';
+
 (*"Resolve" version.  Note: res_inst_tac cannot behave sensibly if the
   terms that are substituted contain (term or type) unknowns from the
   goal, because it is unable to instantiate goal unknowns at the same time.
@@ -290,6 +300,9 @@
 fun res_inst_tac sinsts rule i =
     compose_inst_tac sinsts (false, rule, nprems_of rule) i;
 
+fun res_inst_tac' sinsts rule i =
+    compose_inst_tac' sinsts (false, rule, nprems_of rule) i;
+
 (*eresolve elimination version*)
 fun eres_inst_tac sinsts rule i =
     compose_inst_tac sinsts (true, rule, nprems_of rule) i;