# HG changeset patch
# User lcp
# Date 789876225 -3600
# Node ID f5314a7c93f299dbe636859517d069a3cb4c40dd
# Parent  a05e2b5f24c455763bc36afc27c69f679806c333
Renamed single_fun to singleton_fun.

diff -r a05e2b5f24c4 -r f5314a7c93f2 src/ZF/func.ML
--- a/src/ZF/func.ML	Thu Jan 12 03:03:25 1995 +0100
+++ b/src/ZF/func.ML	Thu Jan 12 03:03:45 1995 +0100
@@ -64,7 +64,7 @@
 (*The singleton function*)
 goalw ZF.thy [Pi_def, function_def] "{<a,b>} : {a} -> {b}";
 by (fast_tac eq_cs 1);
-qed "single_fun";
+qed "singleton_fun";
 
 (*** Function Application ***)
 
@@ -355,7 +355,7 @@
 
 goal ZF.thy
     "!!f A B. [| f: A->B;  c~:A |] ==> cons(<c,b>,f) : cons(c,A) -> cons(b,B)";
-by (forward_tac [single_fun RS fun_disjoint_Un] 1);
+by (forward_tac [singleton_fun RS fun_disjoint_Un] 1);
 by (asm_full_simp_tac (FOL_ss addsimps [cons_eq]) 2);
 by (fast_tac eq_cs 1);
 qed "fun_extend";