--- a/src/HOL/Boogie/Tools/boogie_loader.ML Sun Mar 07 11:57:16 2010 +0100
+++ b/src/HOL/Boogie/Tools/boogie_loader.ML Sun Mar 07 12:19:47 2010 +0100
@@ -87,8 +87,8 @@
| NONE =>
let
val args = Name.variant_list [] (replicate arity "'")
- val (T, thy') = ObjectLogic.typedecl (Binding.name isa_name, args,
- mk_syntax name arity) thy
+ val (T, thy') =
+ Object_Logic.typedecl (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