src/HOL/ex/Recdefs.ML
changeset 6451 bc943acc5fda
parent 5655 afd75136b236
child 8415 852c63072334
--- a/src/HOL/ex/Recdefs.ML	Mon Apr 19 17:53:38 1999 +0200
+++ b/src/HOL/ex/Recdefs.ML	Tue Apr 20 14:32:48 1999 +0200
@@ -11,8 +11,7 @@
 
 Goal "(x: set (qsort (ord,l))) = (x: set l)";
 by (res_inst_tac [("u","ord"),("v","l")] qsort.induct 1);
-by (ALLGOALS Asm_simp_tac);
-by (Blast_tac 1);
+by Auto_tac;
 qed "qsort_mem_stable";