1.1 --- a/src/HOL/Boogie/Tools/boogie_loader.ML	Thu Mar 18 23:00:18 2010 +0100
     1.2 +++ b/src/HOL/Boogie/Tools/boogie_loader.ML	Thu Mar 18 23:08:52 2010 +0100
     1.3 @@ -86,7 +86,7 @@
     1.4          SOME type_name => (((name, type_name), log_ex name type_name), thy)
     1.5        | NONE =>
     1.6            let
     1.7 -            val args = Name.variant_list [] (replicate arity "'")
     1.8 +            val args = map (rpair dummyS) (Name.invents Name.context "'a" arity)
     1.9              val (T, thy') =
    1.10                Typedecl.typedecl_global (Binding.name isa_name, args, mk_syntax name arity) thy
    1.11              val type_name = fst (Term.dest_Type T)