src/HOL/UNITY/Comp/Priority.ML

--- a/src/HOL/UNITY/Comp/Priority.ML	Fri Oct 05 21:50:37 2001 +0200
+++ b/src/HOL/UNITY/Comp/Priority.ML	Fri Oct 05 21:52:39 2001 +0200
@@ -221,7 +221,7 @@
 
 Goal "system: Acyclic leadsTo Highest i";
 by (res_inst_tac [("f", "%s. above i s")] finite_psubset_induct 1);
-by (asm_simp_tac (simpset() delsimps [Highest_def, above_def] 
+by (asm_simp_tac (simpset() delsimps [Highest_def, thm "above_def"]
                             addsimps [Highest_iff_above0,
                                       vimage_def, finite_psubset_def]) 1); 
 by (Clarify_tac 1);