# HG changeset patch
# User haftmann
# Date 1282209564 -7200
# Node ID 8ddfc68a3908efb4ff30e907a0d6bd80907bf101
# Parent  925c4d7b291e4210b90ec41df017ee29ccfa70cb
some more antiquotations

diff -r 925c4d7b291e -r 8ddfc68a3908 src/HOL/Import/hol4rews.ML
--- 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 #>