# HG changeset patch
# User haftmann
# Date 1234361140 -3600
# Node ID 68e9a8d97475cf2391dce5348a1d8e0fd9b6d045
# Parent  7c301075eef101623c0a57829b7d3fdb96b32f93# Parent  4a1510b5f886970f1af45f8552003ac59e1e708d
merged

diff -r 7c301075eef1 -r 68e9a8d97475 doc-src/more_antiquote.ML
--- a/doc-src/more_antiquote.ML	Wed Feb 11 13:47:28 2009 +0100
+++ b/doc-src/more_antiquote.ML	Wed Feb 11 15:05:40 2009 +0100
@@ -93,9 +93,10 @@
     val thy = ProofContext.theory_of ctxt;
     val const = Code_Unit.check_const thy raw_const;
     val (_, funcgr) = Code_Funcgr.make thy [const];
+    fun holize thm = @{thm meta_eq_to_obj_eq} OF [thm];
     val thms = Code_Funcgr.eqns funcgr const
       |> map_filter (fn (thm, linear) => if linear then SOME thm else NONE)
-      |> map (no_vars ctxt o AxClass.overload thy);
+      |> map (holize o no_vars ctxt o AxClass.overload thy);
   in ThyOutput.output_list pretty_thm src ctxt thms end;
 
 in
diff -r 7c301075eef1 -r 68e9a8d97475 src/HOL/Tools/typecopy_package.ML
--- a/src/HOL/Tools/typecopy_package.ML	Wed Feb 11 13:47:28 2009 +0100
+++ b/src/HOL/Tools/typecopy_package.ML	Wed Feb 11 15:05:40 2009 +0100
@@ -115,10 +115,8 @@
     val SOME { constr = constr_name, proj = (proj, _), proj_def = proj_eq, vs = raw_vs,
       typ = raw_ty_rep, ... } =  get_info thy tyco;
     val inst_meet = Sorts.meet_sort_typ (Sign.classes_of thy)
-      (Logic.varifyT raw_ty_rep, [HOLogic.class_eq]);
-    val ty_inst = Logic.varifyT
-      #> inst_meet
-      #> Logic.unvarifyT;
+      (Logic.varifyT raw_ty_rep, [HOLogic.class_eq]) handle Sorts.CLASS_ERROR _ => I;
+    val ty_inst = Logic.unvarifyT o inst_meet o Logic.varifyT;
     val vs = (map dest_TFree o snd o dest_Type o ty_inst)
       (Type (tyco, map TFree raw_vs));
     val ty_rep = ty_inst raw_ty_rep;
@@ -131,7 +129,7 @@
     fun mk_proj t = Const (proj, ty --> ty_rep) $ t;
     val (t_x, t_y) = (Free ("x", ty), Free ("y", ty));
     val def_eq = (HOLogic.mk_Trueprop o HOLogic.mk_eq)
-      (mk_eq ty t_x t_y, mk_eq ty_rep (mk_proj t_x) (mk_proj t_y));
+      (mk_eq ty t_x t_y, HOLogic.mk_eq (mk_proj t_x, mk_proj t_y));
     fun mk_eq_refl thy = @{thm HOL.eq_refl}
       |> Thm.instantiate
          ([pairself (Thm.ctyp_of thy) (TVar (("'a", 0), @{sort eq}), Logic.varifyT ty)], [])
@@ -155,11 +153,8 @@
     |-> (fn refl_thm => Code.add_nonlinear_eqn refl_thm)
   end;
 
-fun perhaps_add_typecopy_default_code tyco thy =
-  add_typecopy_default_code tyco thy handle Sorts.CLASS_ERROR _ => thy;
-
 val setup =
   TypecopyInterpretation.init
-  #> interpretation perhaps_add_typecopy_default_code
+  #> interpretation add_typecopy_default_code
 
 end;