--- a/src/HOL/Tools/Metis/metis_reconstruct.ML Thu Mar 24 17:10:23 2011 +0100
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Thu Mar 24 17:49:27 2011 +0100
@@ -38,6 +38,10 @@
fun verbose_warning ctxt msg =
if Config.get ctxt verbose then warning msg else ()
+val is_zapped_var_name =
+ String.isPrefix Meson_Clausify.new_skolem_var_prefix orf
+ String.isPrefix Meson_Clausify.new_nonskolem_var_prefix
+
datatype term_or_type = SomeTerm of term | SomeType of typ
fun terms_of [] = []
@@ -46,7 +50,7 @@
fun types_of [] = []
| types_of (SomeTerm (Var ((a,idx), _)) :: tts) =
- if String.isPrefix "_" a then
+ if String.isPrefix metis_generated_var_prefix a then
(*Variable generated by Metis, which might have been a type variable.*)
TVar (("'" ^ a, idx), HOLogic.typeS) :: types_of tts
else types_of tts
@@ -656,9 +660,11 @@
| repair t = t
val t' = t |> repair |> fold (curry absdummy) (map snd params)
fun do_instantiate th =
- let val var = Term.add_vars (prop_of th) [] |> the_single in
- th |> term_instantiate thy [(Var var, t')]
- end
+ let
+ val var = Term.add_vars (prop_of th) []
+ |> filter (is_zapped_var_name o fst o fst)
+ |> the_single
+ in th |> term_instantiate thy [(Var var, t')] end
in
(etac @{thm allE} i
THEN rotate_tac ~1 i
@@ -745,6 +751,7 @@
Pattern.first_order_match thy p (Vartab.empty, Vartab.empty)
val tsubst =
tenv |> Vartab.dest
+ |> filter (is_zapped_var_name o fst o fst)
|> sort (cluster_ord
o pairself (Meson_Clausify.cluster_of_zapped_var_name
o fst o fst))
@@ -762,15 +769,13 @@
| _ => raise TERM ("discharge_skolem_premises: Malformed premise",
[prem])
fun cluster_of_var_name skolem s =
- let
- val ((ax_no, (cluster_no, _)), skolem') =
- Meson_Clausify.cluster_of_zapped_var_name s
- in
+ case try Meson_Clausify.cluster_of_zapped_var_name s of
+ NONE => NONE
+ | SOME ((ax_no, (cluster_no, _)), skolem') =>
if skolem' = skolem andalso cluster_no > 0 then
SOME (ax_no, cluster_no)
else
NONE
- end
fun clusters_in_term skolem t =
Term.add_var_names t [] |> map_filter (cluster_of_var_name skolem o fst)
fun deps_for_term_subst (var, t) =
@@ -796,6 +801,7 @@
\\"Hilbert_Choice\"."
val outer_param_names =
[] |> fold (Term.add_var_names o snd) (map_filter I axioms)
+ |> filter (is_zapped_var_name o fst)
|> map (`(Meson_Clausify.cluster_of_zapped_var_name o fst))
|> filter (fn (((_, (cluster_no, _)), skolem), _) =>
cluster_no = 0 andalso skolem)