src/HOL/Tools/typedef_package.ML

     val RepC = Const (full Rep_name, newT --> oldT);
     val AbsC = Const (full Abs_name, oldT --> newT);
     val x_new = Free ("x", newT);
     val y_old = Free ("y", oldT);
 
-    val set' = if no_def then set else setC;    (* FIXME !?? *)
+    val set' = if no_def then set else setC;
 
     val typedef_name = "type_definition_" ^ name;
     val typedefC =
       Const (type_definitionN, (newT --> oldT) --> (oldT --> newT) --> setT --> HOLogic.boolT);
     val typedef_prop = HOLogic.mk_Trueprop (typedefC $ RepC $ AbsC $ set');

         let fun make th = standard (th OF typedef_ax) in
           theory'
           |> (#1 oo PureThy.add_thms)
             ([((Rep_name, make Rep), []),
               ((Rep_name ^ "_inverse", make Rep_inverse), []),
-              ((Abs_name ^ "_inverse", make Abs_inverse), [])] @
-            (if no_def then [] else
-             [((Rep_name ^ "_inject", make Rep_inject), []),
+              ((Abs_name ^ "_inverse", make Abs_inverse), []),
+              ((Rep_name ^ "_inject", make Rep_inject), []),
               ((Abs_name ^ "_inject", make Abs_inject), []),
               ((Rep_name ^ "_cases", make Rep_cases),
                 [RuleCases.case_names [Rep_name], InductAttrib.cases_set_global full_name]),
               ((Abs_name ^ "_cases", make Abs_cases),
                 [RuleCases.case_names [Abs_name], InductAttrib.cases_type_global full_tname]),
               ((Rep_name ^ "_induct", make Rep_induct),
                 [RuleCases.case_names [Rep_name], InductAttrib.induct_set_global full_name]),
               ((Abs_name ^ "_induct", make Abs_induct),
-                [RuleCases.case_names [Abs_name], InductAttrib.induct_type_global full_tname])]))
+                [RuleCases.case_names [Abs_name], InductAttrib.induct_type_global full_tname])])
         end)
       handle ERROR => err_in_typedef name;
 
 
     (* errors *)