1.1 --- a/src/ZF/Perm.ML	Fri Sep 17 12:53:53 1993 +0200
     1.2 +++ b/src/ZF/Perm.ML	Fri Sep 17 16:16:38 1993 +0200
     1.3 @@ -52,6 +52,7 @@
     1.4  (* f: bij(A,B) ==> f: A->B *)
     1.5  val bij_is_fun = standard (bij_is_inj RS inj_is_fun);
     1.6  
     1.7 +
     1.8  (** Identity function **)
     1.9  
    1.10  val [prem] = goalw Perm.thy [id_def] "a:A ==> <a,a> : id(A)";  
    1.11 @@ -76,7 +77,7 @@
    1.12  
    1.13  goalw Perm.thy [inj_def,id_def] "id(A): inj(A,A)";
    1.14  by (REPEAT (ares_tac [CollectI,lam_type] 1));
    1.15 -by (SIMP_TAC ZF_ss 1);
    1.16 +by (simp_tac ZF_ss 1);
    1.17  val id_inj = result();
    1.18  
    1.19  goalw Perm.thy [id_def,surj_def] "id(A): surj(A,A)";
    1.20 @@ -262,7 +263,7 @@
    1.21      "!!f g. [| (f O g): inj(A,C);  g: A->B;  f: B->C |] ==> g: inj(A,B)";
    1.22  by (safe_tac comp_cs);
    1.23  by (REPEAT (eresolve_tac [asm_rl, bspec RS bspec RS mp] 1));
    1.24 -by (ASM_SIMP_TAC (ZF_ss addrews [comp_func_apply]) 1);
    1.25 +by (asm_simp_tac (FOL_ss addsimps [comp_func_apply]) 1);
    1.26  val comp_mem_injD1 = result();
    1.27  
    1.28  goalw Perm.thy [inj_def,surj_def]
    1.29 @@ -271,9 +272,10 @@
    1.30  by (res_inst_tac [("x1", "x")] (bspec RS bexE) 1);
    1.31  by (eres_inst_tac [("x1", "w")] (bspec RS bexE) 3);
    1.32  by (REPEAT (assume_tac 1));
    1.33 -by (safe_tac (comp_cs addSIs ZF_congs));
    1.34 +by (safe_tac comp_cs);
    1.35 +by (res_inst_tac [("t", "op `(g)")] subst_context 1);
    1.36  by (REPEAT (eresolve_tac [asm_rl, bspec RS bspec RS mp] 1));
    1.37 -by (ASM_SIMP_TAC (ZF_ss addrews [comp_func_apply]) 1);
    1.38 +by (asm_simp_tac (FOL_ss addsimps [comp_func_apply]) 1);
    1.39  val comp_mem_injD2 = result();
    1.40  
    1.41  goalw Perm.thy [surj_def]
    1.42 @@ -427,7 +429,9 @@
    1.43  by (etac fun_extend 1);
    1.44  by (REPEAT (ares_tac [ballI] 1));
    1.45  by (REPEAT_FIRST (eresolve_tac [consE,ssubst]));
    1.46 -(*Assumption ALL w:A. ALL x:A. f`w = f`x --> w=x makes ASM_SIMP_TAC loop!*)
    1.47 -by (ALLGOALS (SIMP_TAC (ZF_ss addrews [fun_extend_apply2,fun_extend_apply1])));
    1.48 +(*Assumption ALL w:A. ALL x:A. f`w = f`x --> w=x would make asm_simp_tac loop
    1.49 +  using ZF_ss!  But FOL_ss ignores the assumption...*)
    1.50 +by (ALLGOALS (asm_simp_tac 
    1.51 +	      (FOL_ss addsimps [fun_extend_apply2,fun_extend_apply1])));
    1.52  by (ALLGOALS (fast_tac (ZF_cs addIs [apply_type])));
    1.53  val inj_extend = result();