--- a/src/HOL/Metis_Examples/Type_Encodings.thy Mon Aug 22 15:02:45 2011 +0200
+++ b/src/HOL/Metis_Examples/Type_Encodings.thy Mon Aug 22 15:02:45 2011 +0200
@@ -9,7 +9,7 @@
*}
theory Type_Encodings
-imports Main
+imports "~~/src/HOL/Sledgehammer2d"(*###*)
begin
declare [[metis_new_skolemizer]]
--- a/src/HOL/Tools/ATP/atp_translate.ML Mon Aug 22 15:02:45 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML Mon Aug 22 15:02:45 2011 +0200
@@ -1444,9 +1444,8 @@
fun type_tag_idempotence_fact type_enc =
let
fun var s = ATerm (`I s, [])
- (* Reconstruction in Metis is strangely dependent on these names. *)
- fun tag tm = ATerm (type_tag, [var "T", tm])
- val tagged_var = tag (var "A")
+ fun tag tm = ATerm (type_tag, [var "A", tm])
+ val tagged_var = tag (var "X")
in
Formula (type_tag_idempotence_helper_name, Axiom,
eq_formula type_enc [] false (tag tagged_var) tagged_var,
--- a/src/HOL/Tools/Metis/metis_tactics.ML Mon Aug 22 15:02:45 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_tactics.ML Mon Aug 22 15:02:45 2011 +0200
@@ -78,7 +78,10 @@
let val thy = Proof_Context.theory_of ctxt in
case hol_clause_from_metis ctxt sym_tab old_skolems mth of
Const (@{const_name HOL.eq}, _) $ _ $ t =>
- t |> cterm_of thy |> Thm.reflexive RS @{thm meta_eq_to_obj_eq}
+ let
+ val ct = cterm_of thy t
+ val cT = ctyp_of_term ct
+ in refl |> Drule.instantiate' [SOME cT] [SOME ct] end
| Const (@{const_name disj}, _) $ t1 $ t2 =>
(if can HOLogic.dest_not t1 then t2 else t1)
|> HOLogic.mk_Trueprop |> cterm_of thy |> Thm.trivial