src/HOL/BNF/Tools/bnf_fp_def_sugar.ML

 
     (* TODO: cleaner handling of fake contexts, without "background_theory" *)
     (*the "perhaps o try" below helps gracefully handles the case where the new type is defined in a
       locale and shadows an existing global type*)
 
-    fun add_fake_type spec mixfix =
+    fun add_fake_type spec =
       Sign.add_type no_defs_lthy (type_binding_of spec,
-        length (type_args_named_constrained_of spec), mixfix);
-
-    val fake_thy =
-      Theory.copy #> fold (fn spec => fn thy =>
-          case try (add_fake_type spec (mixfix_of spec)) thy of
-            SOME thy' => thy'
-          | NONE => add_fake_type spec Mixfix.NoSyn thy)
-        specs;
+        length (type_args_named_constrained_of spec), mixfix_of spec);
+
+    val fake_thy = Theory.copy #> fold add_fake_type specs;
     val fake_lthy = Proof_Context.background_theory fake_thy no_defs_lthy;
 
     fun mk_fake_T b =
       Type (fst (Term.dest_Type (Proof_Context.read_type_name fake_lthy true (Binding.name_of b))),
         unsorted_As);