--- a/src/HOL/Tools/Metis/metis_translate.ML Thu Mar 24 17:10:23 2011 +0100
+++ b/src/HOL/Tools/Metis/metis_translate.ML Thu Mar 24 17:49:27 2011 +0100
@@ -36,6 +36,7 @@
tfrees: type_literal list,
old_skolems: (string * term) list}
+ val metis_generated_var_prefix : string
val type_tag_name : string
val bound_var_prefix : string
val schematic_var_prefix: string
@@ -83,6 +84,8 @@
structure Metis_Translate : METIS_TRANSLATE =
struct
+val metis_generated_var_prefix = "_"
+
val type_tag_name = "ti"
val bound_var_prefix = "B_"