src/HOL/Tools/Metis/metis_translate.ML
changeset 40259 c0e34371c2e2
parent 40157 a2f01956220e
child 41138 eb80538166b6
     1.1 --- a/src/HOL/Tools/Metis/metis_translate.ML	Fri Oct 29 12:49:05 2010 +0200
     1.2 +++ b/src/HOL/Tools/Metis/metis_translate.ML	Fri Oct 29 12:49:05 2010 +0200
     1.3 @@ -59,7 +59,7 @@
     1.4    val make_fixed_type_const : string -> string
     1.5    val make_type_class : string -> string
     1.6    val num_type_args: theory -> string -> int
     1.7 -  val new_skolem_var_from_const: string -> indexname
     1.8 +  val new_skolem_var_name_from_const : string -> string
     1.9    val type_literals_for_types : typ list -> type_literal list
    1.10    val make_class_rel_clauses :
    1.11      theory -> class list -> class list -> class_rel_clause list
    1.12 @@ -214,9 +214,9 @@
    1.13    else
    1.14      (s, Sign.the_const_type thy s) |> Sign.const_typargs thy |> length
    1.15  
    1.16 -fun new_skolem_var_from_const s =
    1.17 +fun new_skolem_var_name_from_const s =
    1.18    let val ss = s |> space_explode Long_Name.separator in
    1.19 -    (nth ss (length ss - 2), 0)
    1.20 +    nth ss (length ss - 2)
    1.21    end
    1.22  
    1.23