# HG changeset patch
# User haftmann
# Date 1184081453 -7200
# Node ID 6219d40c4f739b753f3574114fb979332fc04f5b
# Parent  dc452e8641aac3e6b59b20f381bd3abd0c0fb3ad
tuned

diff -r dc452e8641aa -r 6219d40c4f73 src/HOL/Tools/datatype_codegen.ML
--- a/src/HOL/Tools/datatype_codegen.ML	Tue Jul 10 17:30:52 2007 +0200
+++ b/src/HOL/Tools/datatype_codegen.ML	Tue Jul 10 17:30:53 2007 +0200
@@ -453,14 +453,14 @@
   fun constrain_op_eq_thms thy thms =
     let
       fun add_eq (Const ("op =", ty)) =
-            fold (insert (eq_fst (op =)))
-              (Term.add_tvarsT ty [])
+            fold (insert (eq_fst (op =))) (Term.add_tvarsT ty [])
         | add_eq _ =
             I
       val eqs = fold (fold_aterms add_eq o Thm.prop_of) thms [];
       val instT = map (fn (v_i, sort) =>
         (Thm.ctyp_of thy (TVar (v_i, sort)),
-           Thm.ctyp_of thy (TVar (v_i, Sorts.inter_sort (Sign.classes_of thy) (sort, [HOLogic.class_eq]))))) eqs;
+           Thm.ctyp_of thy (TVar (v_i, Sorts.inter_sort (Sign.classes_of thy)
+             (sort, [HOLogic.class_eq]))))) eqs;
     in
       thms
       |> map (Thm.instantiate (instT, []))