src/Pure/drule.ML
changeset 25470 ba5a2bb7a81a
parent 24978 159b0f4dd1e9
child 26424 a6cad32a27b0
equal deleted inserted replaced
25469:f81b3be9dfdd 25470:ba5a2bb7a81a
   828     let val {thy=thyt, t=t, T= T, maxidx=maxt,...} = rep_cterm ct
   828     let val {thy=thyt, t=t, T= T, maxidx=maxt,...} = rep_cterm ct
   829         and {thy=thyu, t=u, T= U, maxidx=maxu,...} = rep_cterm cu;
   829         and {thy=thyu, t=u, T= U, maxidx=maxu,...} = rep_cterm cu;
   830         val maxi = Int.max(maxidx, Int.max(maxt, maxu));
   830         val maxi = Int.max(maxidx, Int.max(maxt, maxu));
   831         val thy' = Theory.merge(thy, Theory.merge(thyt, thyu))
   831         val thy' = Theory.merge(thy, Theory.merge(thyt, thyu))
   832         val (tye',maxi') = Sign.typ_unify thy' (T, U) (tye, maxi)
   832         val (tye',maxi') = Sign.typ_unify thy' (T, U) (tye, maxi)
   833           handle Type.TUNIFY => raise TYPE("Ill-typed instantiation", [T,U], [t,u])
   833           handle Type.TUNIFY => raise TYPE ("Ill-typed instantiation:\nType\n" ^
       
   834             Sign.string_of_typ thy' (Envir.norm_type tye T) ^
       
   835             "\nof variable " ^
       
   836             Sign.string_of_term thy' (Term.map_types (Envir.norm_type tye) t) ^
       
   837             "\ncannot be unified with type\n" ^
       
   838             Sign.string_of_typ thy' (Envir.norm_type tye U) ^ "\nof term " ^
       
   839             Sign.string_of_term thy' (Term.map_types (Envir.norm_type tye) u),
       
   840             [T, U], [t, u])
   834     in  (thy', tye', maxi')  end;
   841     in  (thy', tye', maxi')  end;
   835 in
   842 in
   836 fun cterm_instantiate [] th = th
   843 fun cterm_instantiate [] th = th
   837   | cterm_instantiate ctpairs0 th =
   844   | cterm_instantiate ctpairs0 th =
   838   let val (thy,tye,_) = List.foldr add_types (Thm.theory_of_thm th, Vartab.empty, 0) ctpairs0
   845   let val (thy,tye,_) = List.foldr add_types (Thm.theory_of_thm th, Vartab.empty, 0) ctpairs0