# HG changeset patch
# User wenzelm
# Date 1268950132 -3600
# Node ID 7dd9b1162c63b6a57e1aa9f028cd28bcf9af4397
# Parent  9380fab5f4f7247c1bc0ac1b6949d201e8b2cd77
typedecl: no sort constraints;
prefer Name.invents over old-style Name.variant_list;

diff -r 9380fab5f4f7 -r 7dd9b1162c63 src/HOL/Boogie/Tools/boogie_loader.ML
--- 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)