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