src/HOL/Boogie/Tools/boogie_loader.ML
changeset 35625 9c818cab0dd0
parent 35391 34d8e0a9bfa7
child 35626 06197484c6ad
     1.1 --- a/src/HOL/Boogie/Tools/boogie_loader.ML	Sun Mar 07 11:57:16 2010 +0100
     1.2 +++ b/src/HOL/Boogie/Tools/boogie_loader.ML	Sun Mar 07 12:19:47 2010 +0100
     1.3 @@ -87,8 +87,8 @@
     1.4        | NONE =>
     1.5            let
     1.6              val args = Name.variant_list [] (replicate arity "'")
     1.7 -            val (T, thy') = ObjectLogic.typedecl (Binding.name isa_name, args,
     1.8 -              mk_syntax name arity) thy
     1.9 +            val (T, thy') =
    1.10 +              Object_Logic.typedecl (Binding.name isa_name, args, mk_syntax name arity) thy
    1.11              val type_name = fst (Term.dest_Type T)
    1.12            in (((name, type_name), log_new name type_name), thy') end)
    1.13      end