--- a/src/HOL/Boogie/Tools/boogie_loader.ML Wed Jun 08 22:16:21 2011 +0200
+++ b/src/HOL/Boogie/Tools/boogie_loader.ML Thu Jun 09 20:22:22 2011 +0200
@@ -86,7 +86,7 @@
SOME type_name => (((name, type_name), log_ex name type_name), thy)
| NONE =>
let
- val args = map (rpair dummyS) (Name.invents Name.context "'a" arity)
+ val args = map (rpair dummyS) (Name.invent 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)