# HG changeset patch
# User blanchet
# Date 1286379847 -7200
# Node ID d42ddd7407ca4efd0bff1b3e378ae34983fb9f75
# Parent  415556559fada985515b22b23cbaa657334f394f
qualify "Meson." and "Metis." constants so that the ML files can be reloaded later (e.g. for testing/development)

diff -r 415556559fad -r d42ddd7407ca src/HOL/Tools/Meson/meson_clausify.ML
--- a/src/HOL/Tools/Meson/meson_clausify.ML	Wed Oct 06 17:42:57 2010 +0200
+++ b/src/HOL/Tools/Meson/meson_clausify.ML	Wed Oct 06 17:44:07 2010 +0200
@@ -48,7 +48,7 @@
 
 fun mk_old_skolem_term_wrapper t =
   let val T = fastype_of t in
-    Const (@{const_name skolem}, T --> T) $ t
+    Const (@{const_name Meson.skolem}, T --> T) $ t
   end
 
 fun beta_eta_in_abs_body (Abs (s, T, t')) = Abs (s, T, beta_eta_in_abs_body t')
@@ -91,7 +91,7 @@
          $ _ $ Abs _) => extensionalize_theorem (th RS fun_cong_all)
   | _ => th
 
-fun is_quasi_lambda_free (Const (@{const_name skolem}, _) $ _) = true
+fun is_quasi_lambda_free (Const (@{const_name Meson.skolem}, _) $ _) = true
   | is_quasi_lambda_free (t1 $ t2) =
     is_quasi_lambda_free t1 andalso is_quasi_lambda_free t2
   | is_quasi_lambda_free (Abs _) = false
@@ -348,9 +348,9 @@
            | p => p)
     fun intr_imp ct th =
       Thm.instantiate ([], map (pairself (cterm_of thy))
-                               [(Var (("i", 1), @{typ nat}),
+                               [(Var (("i", 0), @{typ nat}),
                                  HOLogic.mk_nat ax_no)])
-                      @{thm skolem_COMBK_D}
+                      (zero_var_indexes @{thm skolem_COMBK_D})
       RS Thm.implies_intr ct th
   in
     (opt |> Option.map (I #>> singleton (Variable.export ctxt ctxt0)
diff -r 415556559fad -r d42ddd7407ca src/HOL/Tools/Metis/metis_translate.ML
--- a/src/HOL/Tools/Metis/metis_translate.ML	Wed Oct 06 17:42:57 2010 +0200
+++ b/src/HOL/Tools/Metis/metis_translate.ML	Wed Oct 06 17:44:07 2010 +0200
@@ -111,7 +111,7 @@
                (@{const_name HOL.disj}, "or"),
                (@{const_name HOL.implies}, "implies"),
                (@{const_name Set.member}, "member"),
-               (@{const_name fequal}, "fequal"),
+               (@{const_name Metis.fequal}, "fequal"),
                (@{const_name Meson.COMBI}, "COMBI"),
                (@{const_name Meson.COMBK}, "COMBK"),
                (@{const_name Meson.COMBB}, "COMBB"),