1.1 --- a/src/HOL/Import/hol4rews.ML	Thu Aug 19 11:13:07 2010 +0200
     1.2 +++ b/src/HOL/Import/hol4rews.ML	Thu Aug 19 11:19:24 2010 +0200
     1.3 @@ -624,12 +624,12 @@
     1.4  
     1.5  local
     1.6      fun initial_maps thy =
     1.7 -        thy |> add_hol4_type_mapping "min" "bool" false "bool"
     1.8 +        thy |> add_hol4_type_mapping "min" "bool" false @{type_name bool}
     1.9              |> add_hol4_type_mapping "min" "fun" false "fun"
    1.10 -            |> add_hol4_type_mapping "min" "ind" false "Nat.ind"
    1.11 -            |> add_hol4_const_mapping "min" "=" false "op ="
    1.12 -            |> add_hol4_const_mapping "min" "==>" false "op -->"
    1.13 -            |> add_hol4_const_mapping "min" "@" false "Hilbert_Choice.Eps"
    1.14 +            |> add_hol4_type_mapping "min" "ind" false @{type_name ind}
    1.15 +            |> add_hol4_const_mapping "min" "=" false @{const_name "op ="}
    1.16 +            |> add_hol4_const_mapping "min" "==>" false @{const_name "op -->"}
    1.17 +            |> add_hol4_const_mapping "min" "@" false @{const_name "Eps"}
    1.18  in
    1.19  val hol4_setup =
    1.20    initial_maps #>