src/HOL/TLA/Action.thy

--- a/src/HOL/TLA/Action.thy	Sat Mar 22 19:33:39 2014 +0100
+++ b/src/HOL/TLA/Action.thy	Sat Mar 22 20:42:16 2014 +0100
@@ -117,7 +117,7 @@
 
 fun action_use ctxt th =
     case (concl_of th) of
-      Const _ $ (Const ("Intensional.Valid", _) $ _) =>
+      Const _ $ (Const (@{const_name Valid}, _) $ _) =>
               (flatten (action_unlift ctxt th) handle THM _ => th)
     | _ => th;
 *}