tidied using new "inst" rule

--- a/src/ZF/AC/WO6_WO1.ML	Wed Mar 22 12:33:34 2000 +0100
+++ b/src/ZF/AC/WO6_WO1.ML	Wed Mar 22 12:45:41 2000 +0100
@@ -113,11 +113,10 @@
 by (REPEAT (fast_tac (claset() addSEs [LeastI]) 1));
 qed "nested_LeastI";
 
-val nested_Least_instance = 
-   standard
-     (read_instantiate 
-        [("P","%g d. domain(uu(f,b,g,d)) ~= 0 &  \
-\               domain(uu(f,b,g,d)) lepoll m")] nested_LeastI);
+bind_thm ("nested_Least_instance",
+	  inst "P" 
+               "%g d. domain(uu(f,b,g,d)) ~= 0 & domain(uu(f,b,g,d)) lepoll m" 
+	  nested_LeastI);
 
 Goalw [gg1_def]
     "!!a. [| Ord(a);  m:nat;  \

--- a/src/ZF/Arith.ML	Wed Mar 22 12:33:34 2000 +0100
+++ b/src/ZF/Arith.ML	Wed Mar 22 12:45:41 2000 +0100
@@ -246,8 +246,8 @@
 qed "diff_cancel";
 
 Goal "[| k:nat; m: nat; n: nat |] ==> (m#+k) #- (n#+k) = m #- n";
-val add_commute_k = read_instantiate [("n","k")] add_commute;
-by (asm_simp_tac (simpset() addsimps [add_commute_k, diff_cancel]) 1);
+by (asm_simp_tac
+    (simpset() addsimps [inst "n" "k" add_commute, diff_cancel]) 1);
 qed "diff_cancel2";
 
 Goal "[| m:nat;  n:nat |] ==> n #- (n#+m) = 0";
@@ -263,9 +263,8 @@
 qed "diff_mult_distrib" ;
 
 Goal "[| m:nat; n: nat; k:nat |] ==> k #* (m #- n) = (k #* m) #- (k #* n)";
-val mult_commute_k = read_instantiate [("m","k")] mult_commute;
-by (asm_simp_tac (simpset() addsimps 
-                  [mult_commute_k, diff_mult_distrib]) 1);
+by (asm_simp_tac
+    (simpset() addsimps [inst "m" "k" mult_commute, diff_mult_distrib]) 1);
 qed "diff_mult_distrib2" ;
 
 (*** Remainder ***)

--- a/src/ZF/CardinalArith.ML	Wed Mar 22 12:33:34 2000 +0100
+++ b/src/ZF/CardinalArith.ML	Wed Mar 22 12:45:41 2000 +0100
@@ -291,7 +291,7 @@
 Goal "Card(n) ==> 2 |*| n = n |+| n";
 by (asm_simp_tac 
     (simpset() addsimps [cmult_succ_lemma, Card_is_Ord,
-			 read_instantiate [("j","0")] cadd_commute]) 1);
+			 inst "j" "0" cadd_commute]) 1);
 qed "cmult_2";
 
 

--- a/src/ZF/Ordinal.ML	Wed Mar 22 12:33:34 2000 +0100
+++ b/src/ZF/Ordinal.ML	Wed Mar 22 12:45:41 2000 +0100
@@ -573,8 +573,7 @@
 
 val [ordi,ordj,ordk] = goal Ordinal.thy
     "[| Ord(i); Ord(j); Ord(k) |] ==> i Un j : k  <->  i:k & j:k";
-by (cut_facts_tac [[ordi,ordj] MRS 
-                   read_instantiate [("k","k")] Un_least_lt_iff] 1);
+by (cut_inst_tac [("k","k")] ([ordi,ordj] MRS Un_least_lt_iff) 1);
 by (asm_full_simp_tac (simpset() addsimps [lt_def,ordi,ordj,ordk]) 1);
 qed "Un_least_mem_iff";
 

--- a/src/ZF/Perm.ML	Wed Mar 22 12:33:34 2000 +0100
+++ b/src/ZF/Perm.ML	Wed Mar 22 12:45:41 2000 +0100
@@ -245,7 +245,7 @@
 bind_thm ("compEpair", 
     rule_by_tactic (REPEAT_FIRST (etac Pair_inject ORELSE' bound_hyp_subst_tac)
                     THEN prune_params_tac)
-        (read_instantiate [("xz","<a,c>")] compE));
+        (inst "xz" "<a,c>" compE));
 
 AddSIs [idI];
 AddIs  [compI];

--- a/src/ZF/QPair.ML	Wed Mar 22 12:33:34 2000 +0100
+++ b/src/ZF/QPair.ML	Wed Mar 22 12:45:41 2000 +0100
@@ -67,7 +67,7 @@
 val QSigmaE2 = 
   rule_by_tactic (REPEAT_FIRST (etac QPair_inject ORELSE' bound_hyp_subst_tac)
                   THEN prune_params_tac)
-      (read_instantiate [("c","<a;b>")] QSigmaE);  
+      (inst "c" "<a;b>" QSigmaE);  
 
 qed_goal "QSigmaD1" thy "<a;b> : QSigma(A,B) ==> a : A"
  (fn [major]=>

--- a/src/ZF/ex/Limit.ML	Wed Mar 22 12:33:34 2000 +0100
+++ b/src/ZF/ex/Limit.ML	Wed Mar 22 12:45:41 2000 +0100
@@ -1782,8 +1782,9 @@
 by (etac leE 1);
 by (asm_simp_tac(simpset() addsimps[e_less_eq,e_gr_eq]) 2);
 (* Must control rewriting by instantiating a variable. *)
-by (asm_full_simp_tac(simpset() addsimps
-     [read_instantiate [("i1","n")] (nat_into_Ord RS not_le_iff_lt RS iff_sym),
+by (asm_full_simp_tac
+    (simpset() addsimps
+     [inst "i1" "n" (nat_into_Ord RS not_le_iff_lt RS iff_sym),
       add_le_self]) 1);
 qed "eps_e_gr_add";
 
@@ -2488,8 +2489,9 @@
 by (res_inst_tac[("b","t")](lub_const RS subst) 2);
 by (stac comp_lubs 4);
 by (asm_simp_tac (simpset() addsimps [comp_assoc, 
-			   read_instantiate [("f","f")] mediating_eq]) 9);
-brr[cont_fun, emb_cont, mediating_emb, cont_cf, cpo_cf, chain_const, commute_chain,emb_chain_cpo] 1;
+				      inst "f" "f" mediating_eq]) 9);
+brr[cont_fun, emb_cont, mediating_emb, cont_cf, cpo_cf, chain_const, 
+    commute_chain,emb_chain_cpo] 1;
 qed "lub_universal_unique";
 
 (*---------------------------------------------------------------------*)

--- a/src/ZF/upair.ML	Wed Mar 22 12:33:34 2000 +0100
+++ b/src/ZF/upair.ML	Wed Mar 22 12:45:41 2000 +0100
@@ -272,11 +272,11 @@
 	addsplits[split_if]
 **)
 
-bind_thm ("split_if_eq1", read_instantiate [("P", "%x. x = ?b")] split_if);
-bind_thm ("split_if_eq2", read_instantiate [("P", "%x. ?a = x")] split_if);
+bind_thm ("split_if_eq1", inst "P" "%x. x = ?b" split_if);
+bind_thm ("split_if_eq2", inst "P" "%x. ?a = x" split_if);
 
-bind_thm ("split_if_mem1", read_instantiate [("P", "%x. x : ?b")] split_if);
-bind_thm ("split_if_mem2", read_instantiate [("P", "%x. ?a : x")] split_if);
+bind_thm ("split_if_mem1", inst "P" "%x. x : ?b" split_if);
+bind_thm ("split_if_mem2", inst "P" "%x. ?a : x" split_if);
 
 val split_ifs = [split_if_eq1, split_if_eq2,
 		 split_if_mem1, split_if_mem2];