src/HOL/Wellfounded_Relations.ML

 qed "wf_weak_decr_stable";
 
 (* special case: <= *)
 
 Goal "(m, n) : pred_nat^* = (m <= n)";
-by (simp_tac (simpset() addsimps [less_eq, reflcl_trancl RS sym] 
-                        delsimps [reflcl_trancl]) 1);
+by (simp_tac (simpset() addsimps [less_eq, thm"reflcl_trancl" RS sym] 
+                        delsimps [thm"reflcl_trancl"]) 1);
 by (arith_tac 1);
 qed "le_eq";
 
 Goal "ALL i. f (Suc i) <= ((f i)::nat) ==> EX i. ALL k. f (i+k) = f i";
 by (res_inst_tac [("r","pred_nat")] wf_weak_decr_stable 1);