--- a/src/HOL/Import/hol4rews.ML Thu Aug 19 11:13:07 2010 +0200
+++ b/src/HOL/Import/hol4rews.ML Thu Aug 19 11:19:24 2010 +0200
@@ -624,12 +624,12 @@
local
fun initial_maps thy =
- thy |> add_hol4_type_mapping "min" "bool" false "bool"
+ thy |> add_hol4_type_mapping "min" "bool" false @{type_name bool}
|> add_hol4_type_mapping "min" "fun" false "fun"
- |> add_hol4_type_mapping "min" "ind" false "Nat.ind"
- |> add_hol4_const_mapping "min" "=" false "op ="
- |> add_hol4_const_mapping "min" "==>" false "op -->"
- |> add_hol4_const_mapping "min" "@" false "Hilbert_Choice.Eps"
+ |> add_hol4_type_mapping "min" "ind" false @{type_name ind}
+ |> add_hol4_const_mapping "min" "=" false @{const_name "op ="}
+ |> add_hol4_const_mapping "min" "==>" false @{const_name "op -->"}
+ |> add_hol4_const_mapping "min" "@" false @{const_name "Eps"}
in
val hol4_setup =
initial_maps #>