# HG changeset patch
# User blanchet
# Date 1346925323 -7200
# Node ID 592a81b4d41339fd604fb891d026c6c05b241f93
# Parent  f9d48d479c843f53d35ab1bff9c10459ddb4bb10
use "add_type" rather than "add_types_global"

diff -r f9d48d479c84 -r 592a81b4d413 src/HOL/Codatatype/Tools/bnf_fp_sugar.ML
--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Thu Sep 06 11:51:19 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Thu Sep 06 11:55:23 2012 +0200
@@ -277,8 +277,8 @@
 fun data_cmd info specs lthy =
   let
     val fake_thy = Theory.copy
-      #> Sign.add_types_global (map (fn spec =>
-        (type_binder_of spec, length (type_args_constrained_of spec), mixfix_of_typ spec)) specs);
+      #> fold (fn spec => Sign.add_type lthy
+        (type_binder_of spec, length (type_args_constrained_of spec), mixfix_of_typ spec)) specs;
     val fake_lthy = Proof_Context.background_theory fake_thy lthy;
   in
     prepare_data Syntax.read_typ info specs fake_lthy lthy