src/CCL/Wfd.thy
changeset 27146 443c19953137
parent 26391 6e8aa5a4eb82
child 27208 5fe899199f85
--- a/src/CCL/Wfd.thy	Wed Jun 11 11:20:10 2008 +0200
+++ b/src/CCL/Wfd.thy	Wed Jun 11 15:40:20 2008 +0200
@@ -54,10 +54,8 @@
   done
 
 ML {*
-  local val wfd_strengthen_lemma = thm "wfd_strengthen_lemma" in
   fun wfd_strengthen_tac s i =
-    res_inst_tac [("Q",s)] wfd_strengthen_lemma i THEN assume_tac (i+1)
-  end
+    res_inst_tac [("Q",s)] @{thm wfd_strengthen_lemma} i THEN assume_tac (i+1)
 *}
 
 lemma wf_anti_sym: "[| Wfd(r);  <a,x>:r;  <x,a>:r |] ==> P"