qualify "Meson." and "Metis." constants so that the ML files can be reloaded later (e.g. for testing/development)
authorblanchet
Wed Oct 06 17:44:07 2010 +0200 (2010-10-06)
changeset 39962d42ddd7407ca
parent 39961 415556559fad
child 39963 626b1d360d42
qualify "Meson." and "Metis." constants so that the ML files can be reloaded later (e.g. for testing/development)
src/HOL/Tools/Meson/meson_clausify.ML
src/HOL/Tools/Metis/metis_translate.ML
     1.1 --- a/src/HOL/Tools/Meson/meson_clausify.ML	Wed Oct 06 17:42:57 2010 +0200
     1.2 +++ b/src/HOL/Tools/Meson/meson_clausify.ML	Wed Oct 06 17:44:07 2010 +0200
     1.3 @@ -48,7 +48,7 @@
     1.4  
     1.5  fun mk_old_skolem_term_wrapper t =
     1.6    let val T = fastype_of t in
     1.7 -    Const (@{const_name skolem}, T --> T) $ t
     1.8 +    Const (@{const_name Meson.skolem}, T --> T) $ t
     1.9    end
    1.10  
    1.11  fun beta_eta_in_abs_body (Abs (s, T, t')) = Abs (s, T, beta_eta_in_abs_body t')
    1.12 @@ -91,7 +91,7 @@
    1.13           $ _ $ Abs _) => extensionalize_theorem (th RS fun_cong_all)
    1.14    | _ => th
    1.15  
    1.16 -fun is_quasi_lambda_free (Const (@{const_name skolem}, _) $ _) = true
    1.17 +fun is_quasi_lambda_free (Const (@{const_name Meson.skolem}, _) $ _) = true
    1.18    | is_quasi_lambda_free (t1 $ t2) =
    1.19      is_quasi_lambda_free t1 andalso is_quasi_lambda_free t2
    1.20    | is_quasi_lambda_free (Abs _) = false
    1.21 @@ -348,9 +348,9 @@
    1.22             | p => p)
    1.23      fun intr_imp ct th =
    1.24        Thm.instantiate ([], map (pairself (cterm_of thy))
    1.25 -                               [(Var (("i", 1), @{typ nat}),
    1.26 +                               [(Var (("i", 0), @{typ nat}),
    1.27                                   HOLogic.mk_nat ax_no)])
    1.28 -                      @{thm skolem_COMBK_D}
    1.29 +                      (zero_var_indexes @{thm skolem_COMBK_D})
    1.30        RS Thm.implies_intr ct th
    1.31    in
    1.32      (opt |> Option.map (I #>> singleton (Variable.export ctxt ctxt0)
     2.1 --- a/src/HOL/Tools/Metis/metis_translate.ML	Wed Oct 06 17:42:57 2010 +0200
     2.2 +++ b/src/HOL/Tools/Metis/metis_translate.ML	Wed Oct 06 17:44:07 2010 +0200
     2.3 @@ -111,7 +111,7 @@
     2.4                 (@{const_name HOL.disj}, "or"),
     2.5                 (@{const_name HOL.implies}, "implies"),
     2.6                 (@{const_name Set.member}, "member"),
     2.7 -               (@{const_name fequal}, "fequal"),
     2.8 +               (@{const_name Metis.fequal}, "fequal"),
     2.9                 (@{const_name Meson.COMBI}, "COMBI"),
    2.10                 (@{const_name Meson.COMBK}, "COMBK"),
    2.11                 (@{const_name Meson.COMBB}, "COMBB"),