744   | _ =>

   744 

   745       let

   745   | (t $ s, t' $ s') =>  

   746         val (qhead, qargs) = strip_comb qtrm

   746        (inj_repabs_trm lthy (t, t')) $ (inj_repabs_trm lthy (s, s'))

   747         val (rhead, rargs) = strip_combn (length qargs) rtrm

   747 

   748         val rargs' = map (inj_repabs_trm lthy) (rargs ~~ qargs)

   748   | (Free (x, T), Free (x', T')) => 

   749       in

   749         if T = T' 

   750         case (rhead, qhead) of

   750         then rtrm 

   751           (Const (s, T), Const (s', T')) =>

   751         else mk_repabs lthy (T, T') rtrm

   752              if T = T'                    

   752 

   753              then list_comb (rhead, rargs') 

   753   | (Const (s, T), Const (s', T')) =>

   754              else list_comb (mk_repabs lthy (T, T') rhead, rargs') 

   754         if T = T'                    

   755         | (Free (x, T), Free (x', T')) => 

   755         then rtrm

   756              if T = T' 

   756         else mk_repabs lthy (T, T') rtrm

   757              then list_comb (rhead, rargs')

   757   

   758              else list_comb (mk_repabs lthy (T, T') rhead, rargs')

   758   | (_, Const (@{const_name "op ="}, _)) => rtrm

   759         | (Abs _, Abs _) =>

   759   

   760              list_comb (inj_repabs_trm lthy (rhead, qhead), rargs') 

   760   | _ => raise (LIFT_MATCH "injection")

   761  

   762         (* FIXME: when there is an (op =), then lhs might have been a term *) 

   763         | (_, Const (@{const_name "op ="}, T)) =>

   764              list_comb (rhead, rargs')

   765         | _ => raise (LIFT_MATCH ("injection: rhead: " ^ (Syntax.string_of_term lthy rhead) 

   766                                           ^ " qhead: " ^ (Syntax.string_of_term lthy qhead)))

   767       end