883     ])

   883     ])

   884 *}

   884 *}

   885 

   885 

   886 

   886 

   887 

   887 

   893 

   890 

   894 (* changes (?'a ?'b raw) (?'a ?'b quo) (int 'b raw \<Rightarrow> bool) to (int 'b quo \<Rightarrow> bool) *)

   891 (* changes (?'a ?'b raw) (?'a ?'b quo) (int 'b raw \<Rightarrow> bool) to (int 'b quo \<Rightarrow> bool) *)

   895 ML {*

   892 ML {*

   896 fun exchange_ty lthy rty qty ty =

   893 fun exchange_ty lthy rty qty ty =

   897   let

   894   let