--- 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