src/ZF/Perm.ML

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