src/HOL/TLA/Intensional.thy
changeset 59582 0fbed69ff081
parent 58950 d07464875dd4
child 60587 0318b43ee95c
     1.1 --- a/src/HOL/TLA/Intensional.thy	Tue Mar 03 19:08:04 2015 +0100
     1.2 +++ b/src/HOL/TLA/Intensional.thy	Wed Mar 04 19:53:18 2015 +0100
     1.3 @@ -271,18 +271,18 @@
     1.4      fun matchsome tha thb =
     1.5        let fun hmatch 0 = raise THM("matchsome: no match", 0, [tha,thb])
     1.6              | hmatch n = matchres tha n thb handle THM _ => hmatch (n-1)
     1.7 -      in hmatch (nprems_of thb) end
     1.8 +      in hmatch (Thm.nprems_of thb) end
     1.9  
    1.10      fun hflatten t =
    1.11 -        case (concl_of t) of
    1.12 -          Const _ $ (Const (@{const_name HOL.implies}, _) $ _ $ _) => hflatten (t RS mp)
    1.13 -        | _ => (hflatten (matchsome conjI t)) handle THM _ => zero_var_indexes t
    1.14 +      case Thm.concl_of t of
    1.15 +        Const _ $ (Const (@{const_name HOL.implies}, _) $ _ $ _) => hflatten (t RS mp)
    1.16 +      | _ => (hflatten (matchsome conjI t)) handle THM _ => zero_var_indexes t
    1.17    in
    1.18      hflatten t
    1.19    end
    1.20  
    1.21  fun int_use ctxt th =
    1.22 -    case (concl_of th) of
    1.23 +    case Thm.concl_of th of
    1.24        Const _ $ (Const (@{const_name Valid}, _) $ _) =>
    1.25                (flatten (int_unlift ctxt th) handle THM _ => th)
    1.26      | _ => th