typedecl: no sort constraints;
prefer Name.invents over old-style Name.variant_list;

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