diff -r cbc38731d42f -r 0fbed69ff081 src/HOL/TLA/Action.thy
--- a/src/HOL/TLA/Action.thy	Tue Mar 03 19:08:04 2015 +0100
+++ b/src/HOL/TLA/Action.thy	Wed Mar 04 19:53:18 2015 +0100
@@ -116,7 +116,7 @@
 val action_rewrite = int_rewrite
 
 fun action_use ctxt th =
-    case (concl_of th) of
+    case Thm.concl_of th of
       Const _ $ (Const (@{const_name Valid}, _) $ _) =>
               (flatten (action_unlift ctxt th) handle THM _ => th)
     | _ => th;