tuning
authorblanchet
Fri Jun 10 17:52:09 2011 +0200 (2011-06-10)
changeset 433592db277c6d506
parent 43358 ff6cfa33c653
child 43360 6f14d1386a1e
tuning
src/HOL/Tools/Metis/metis_reconstruct.ML
     1.1 --- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Fri Jun 10 17:37:50 2011 +0200
     1.2 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Fri Jun 10 17:52:09 2011 +0200
     1.3 @@ -180,14 +180,14 @@
     1.4  fun resolve_inc_tyvars thy tha i thb =
     1.5    let
     1.6      val tha = incr_type_indexes (1 + Thm.maxidx_of thb) tha
     1.7 -    fun aux tha thb =
     1.8 +    fun aux (tha, thb) =
     1.9        case Thm.bicompose false (false, tha, nprems_of tha) i thb
    1.10             |> Seq.list_of |> distinct Thm.eq_thm of
    1.11          [th] => th
    1.12        | _ => raise THM ("resolve_inc_tyvars: unique result expected", i,
    1.13                          [tha, thb])
    1.14    in
    1.15 -    aux tha thb
    1.16 +    aux (tha, thb)
    1.17      handle TERM z =>
    1.18             (* The unifier, which is invoked from "Thm.bicompose", will sometimes
    1.19                refuse to unify "?a::?'a" with "?a::?'b" or "?a::nat" and throw a
    1.20 @@ -206,7 +206,8 @@
    1.21                     |> map (fn (x, (S, T)) =>
    1.22                                pairself (ctyp_of thy) (TVar (x, S), T)) of
    1.23               [] => raise TERM z
    1.24 -           | ps => aux (Drule.instantiate_normalize (ps, []) tha) (Drule.instantiate_normalize (ps, []) thb)
    1.25 +           | ps => (tha, thb) |> pairself (Drule.instantiate_normalize (ps, []))
    1.26 +                              |> aux
    1.27    end
    1.28  
    1.29  fun s_not (@{const Not} $ t) = t