# HG changeset patch
# User blanchet
# Date 1346926893 -7200
# Node ID 83fdea0c477911bf6059574d18f76e13cc68ba1d
# Parent  0cc46e2dee7ed1c78c2ca5ea67c2868c70667957
gracefully handle shadowing case (fourth step of sugar localization)

diff -r 0cc46e2dee7e -r 83fdea0c4779 src/HOL/Codatatype/Tools/bnf_fp_sugar.ML
--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Thu Sep 06 12:14:40 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Thu Sep 06 12:21:33 2012 +0200
@@ -279,9 +279,11 @@
 
 fun data_cmd info specs lthy =
   let
+    (*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*)
     val fake_thy = Theory.copy
-      #> fold (fn spec => Sign.add_type lthy
-        (type_binder_of spec, length (type_args_constrained_of spec), mixfix_of spec)) specs;
+      #> fold (fn spec => perhaps (try (Sign.add_type lthy
+        (type_binder_of spec, length (type_args_constrained_of spec), mixfix_of spec)))) specs;
     val fake_lthy = Proof_Context.background_theory fake_thy lthy;
   in
     prepare_data Syntax.read_typ info specs fake_lthy lthy