# HG changeset patch
# User blanchet
# Date 1366836502 -7200
# Node ID d2a236b10796675b7e463deaa57ee79382a87622
# Parent  bbcdd8519253b3b0fdcf5e60e5d8619207cb0bbb
proper error generated for wrong mixfix

diff -r bbcdd8519253 -r d2a236b10796 src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Wed Apr 24 18:49:52 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Wed Apr 24 22:48:22 2013 +0200
@@ -183,9 +183,16 @@
     (* 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 =
+      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 => perhaps (try (Sign.add_type no_defs_lthy
-          (type_binding_of spec, length (type_args_named_constrained_of spec), mixfix_of spec))))
+      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_lthy = Proof_Context.background_theory fake_thy no_defs_lthy;