1.1 --- a/src/HOL/ex/reflection.ML	Fri Jan 26 13:59:06 2007 +0100
     1.2 +++ b/src/HOL/ex/reflection.ML	Sun Jan 28 11:52:52 2007 +0100
     1.3 @@ -38,7 +38,7 @@
     1.4     val (((_,_),[th']), ctxt') = Variable.import true [th] ctxt
     1.5     val (lhs, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.prop_of th'))
     1.6     fun add_fterms (t as t1 $ t2) = 
     1.7 -       if exists (fn f => (t |> strip_comb |> fst) aconv f) fs then insert (op aconv) t
     1.8 +       if exists (fn f => could_unify (t |> strip_comb |> fst, f)) fs then insert (op aconv) t
     1.9         else add_fterms t1 #> add_fterms t2
    1.10       | add_fterms (t as Abs(xn,xT,t')) = 
    1.11         if (fN mem (term_consts t)) then (fn _ => [t]) else (fn _ => [])
    1.12 @@ -92,7 +92,7 @@
    1.13   let 
    1.14    val tt = HOLogic.listT (fastype_of t)
    1.15   in 
    1.16 -  (case AList.lookup (op =) (!bds) tt of
    1.17 +  (case AList.lookup Type.could_unify (!bds) tt of
    1.18      NONE => error "index_of : type not found in environements!"
    1.19    | SOME (tbs,tats) =>
    1.20      let
    1.21 @@ -160,8 +160,8 @@
    1.22     in exists_Const 
    1.23  	  (fn (n,ty) => n="List.nth" 
    1.24  			andalso 
    1.25 -			AList.defined (op =) (!bds) (domain_type ty)) rhs 
    1.26 -	  andalso fastype_of rhs = tT
    1.27 +			AList.defined Type.could_unify (!bds) (domain_type ty)) rhs 
    1.28 +	  andalso Type.could_unify (fastype_of rhs, tT)
    1.29     end
    1.30    fun get_nth t = 
    1.31     case t of