src/CCL/Wfd.thy
changeset 32283 3bebc195c124
parent 32282 853ef99c04cc
child 33317 b4534348b8fd
--- a/src/CCL/Wfd.thy	Thu Jul 30 11:23:57 2009 +0200
+++ b/src/CCL/Wfd.thy	Thu Jul 30 12:20:43 2009 +0200
@@ -499,7 +499,7 @@
 in
 
 fun eval_tac ths =
-  FOCUS_PREMS (fn {context, prems, ...} =>
+  Subgoal.FOCUS_PREMS (fn {context, prems, ...} =>
     DEPTH_SOLVE_1 (resolve_tac (ths @ prems @ Data.get context) 1));
 
 val eval_setup =