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]