src/ZF/QPair.ML

--- 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]=>