# HG changeset patch
# User wenzelm
# Date 1268173969 -3600
# Node ID 5e6811f4294b2ee290179faf0e77d98eab410e9c
# Parent  8b22a498b034a5922c89e8d5c492a80940da3f45
Typedecl.typedecl_global;

diff -r 8b22a498b034 -r 5e6811f4294b src/HOL/Boogie/Tools/boogie_loader.ML
--- a/src/HOL/Boogie/Tools/boogie_loader.ML	Tue Mar 09 23:32:13 2010 +0100
+++ b/src/HOL/Boogie/Tools/boogie_loader.ML	Tue Mar 09 23:32:49 2010 +0100
@@ -88,7 +88,7 @@
           let
             val args = Name.variant_list [] (replicate arity "'")
             val (T, thy') =
-              Typedecl.typedecl (Binding.name isa_name, args, mk_syntax name arity) thy
+              Typedecl.typedecl_global (Binding.name isa_name, args, mk_syntax name arity) thy
             val type_name = fst (Term.dest_Type T)
           in (((name, type_name), log_new name type_name), thy') end)
     end
diff -r 8b22a498b034 -r 5e6811f4294b src/HOL/Tools/typedef.ML
--- a/src/HOL/Tools/typedef.ML	Tue Mar 09 23:32:13 2010 +0100
+++ b/src/HOL/Tools/typedef.ML	Tue Mar 09 23:32:49 2010 +0100
@@ -130,7 +130,7 @@
           in Drule.export_without_context (Drule.equal_elim_rule2 OF [goal_eq, th]) end;
 
     fun typedef_result inhabited =
-      Typedecl.typedecl (tname, vs, mx)
+      Typedecl.typedecl_global (tname, vs, mx)
       #> snd
       #> Sign.add_consts_i
         [(Rep_name, newT --> oldT, NoSyn),