1.1 --- a/src/HOL/Tools/typecopy_package.ML	Wed Feb 11 15:05:25 2009 +0100
     1.2 +++ b/src/HOL/Tools/typecopy_package.ML	Wed Feb 11 15:05:26 2009 +0100
     1.3 @@ -115,10 +115,8 @@
     1.4      val SOME { constr = constr_name, proj = (proj, _), proj_def = proj_eq, vs = raw_vs,
     1.5        typ = raw_ty_rep, ... } =  get_info thy tyco;
     1.6      val inst_meet = Sorts.meet_sort_typ (Sign.classes_of thy)
     1.7 -      (Logic.varifyT raw_ty_rep, [HOLogic.class_eq]);
     1.8 -    val ty_inst = Logic.varifyT
     1.9 -      #> inst_meet
    1.10 -      #> Logic.unvarifyT;
    1.11 +      (Logic.varifyT raw_ty_rep, [HOLogic.class_eq]) handle Sorts.CLASS_ERROR _ => I;
    1.12 +    val ty_inst = Logic.unvarifyT o inst_meet o Logic.varifyT;
    1.13      val vs = (map dest_TFree o snd o dest_Type o ty_inst)
    1.14        (Type (tyco, map TFree raw_vs));
    1.15      val ty_rep = ty_inst raw_ty_rep;
    1.16 @@ -131,7 +129,7 @@
    1.17      fun mk_proj t = Const (proj, ty --> ty_rep) $ t;
    1.18      val (t_x, t_y) = (Free ("x", ty), Free ("y", ty));
    1.19      val def_eq = (HOLogic.mk_Trueprop o HOLogic.mk_eq)
    1.20 -      (mk_eq ty t_x t_y, mk_eq ty_rep (mk_proj t_x) (mk_proj t_y));
    1.21 +      (mk_eq ty t_x t_y, HOLogic.mk_eq (mk_proj t_x, mk_proj t_y));
    1.22      fun mk_eq_refl thy = @{thm HOL.eq_refl}
    1.23        |> Thm.instantiate
    1.24           ([pairself (Thm.ctyp_of thy) (TVar (("'a", 0), @{sort eq}), Logic.varifyT ty)], [])
    1.25 @@ -155,11 +153,8 @@
    1.26      |-> (fn refl_thm => Code.add_nonlinear_eqn refl_thm)
    1.27    end;
    1.28  
    1.29 -fun perhaps_add_typecopy_default_code tyco thy =
    1.30 -  add_typecopy_default_code tyco thy handle Sorts.CLASS_ERROR _ => thy;
    1.31 -
    1.32  val setup =
    1.33    TypecopyInterpretation.init
    1.34 -  #> interpretation perhaps_add_typecopy_default_code
    1.35 +  #> interpretation add_typecopy_default_code
    1.36  
    1.37  end;