src/HOL/TLA/Action.thy
changeset 59582 0fbed69ff081
parent 59498 50b60f501b05
child 60587 0318b43ee95c
     1.1 --- a/src/HOL/TLA/Action.thy	Tue Mar 03 19:08:04 2015 +0100
     1.2 +++ b/src/HOL/TLA/Action.thy	Wed Mar 04 19:53:18 2015 +0100
     1.3 @@ -116,7 +116,7 @@
     1.4  val action_rewrite = int_rewrite
     1.5  
     1.6  fun action_use ctxt th =
     1.7 -    case (concl_of th) of
     1.8 +    case Thm.concl_of th of
     1.9        Const _ $ (Const (@{const_name Valid}, _) $ _) =>
    1.10                (flatten (action_unlift ctxt th) handle THM _ => th)
    1.11      | _ => th;