diff -r 4d0545e93c0d -r c533bc92e882 WF.ML
--- a/WF.ML	Wed Dec 14 10:32:07 1994 +0100
+++ b/WF.ML	Wed Dec 14 11:17:18 1994 +0100
@@ -111,7 +111,7 @@
 by (REPEAT (rtac impI 1 ORELSE etac ssubst 1));
 by (asm_simp_tac (wf_super_ss addcongs [if_cong]) 1);
 qed "is_recfun_equal_lemma";
-val is_recfun_equal = standard (is_recfun_equal_lemma RS mp RS mp);
+bind_thm ("is_recfun_equal", (is_recfun_equal_lemma RS mp RS mp));
 
 
 val prems as [wfr,transr,recfa,recgb,_] = goalw WF.thy [cut_def]