src/Pure/Tools/codegen_simtype.ML

     fun dest_fun (ty as Type (_, [ty1, ty2])) =
           if is_funtype ty then (ty1, ty2)
           else raise TYPE ("dest_fun", [ty], [])
       | dest_fun ty = raise TYPE ("dest_fun", [ty], []);
     val PROP = ObjectLogic.ensure_propT thy
-    val (ty_abs, ty_rep) = (dest_fun o type_of) repm;
+    val (ty_abs, ty_rep) = (dest_fun o fastype_of) repm;
     val (tyco_abs, ty_parms) = dest_Type ty_abs;
     val _ = if exists (fn TFree _ => false | _ => true) ty_parms then raise TYPE ("no TFree", ty_parms, []) else ();
     val repv = Free ("x", ty_rep);
     val absv = Free ("x", ty_abs);
     val rep_mor = Logic.mk_implies