# HG changeset patch
# User blanchet
# Date 1366872970 -7200
# Node ID 5c657ca97d992a870aec9fb89d24f1f83f2a4679
# Parent  d2a236b10796675b7e463deaa57ee79382a87622
simplified code -- no need for two attempts, the error we get from mixfix the first time is good (and better to get than a parse error in the specification because the user tries to use a mixfix that silently failed)

diff -r d2a236b10796 -r 5c657ca97d99 src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Wed Apr 24 22:48:22 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Thu Apr 25 08:56:10 2013 +0200
@@ -184,16 +184,11 @@
     (*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);
+        length (type_args_named_constrained_of spec), mixfix_of spec);
 
-    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;
+    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 =