# HG changeset patch
# User blanchet
# Date 1338971705 -7200
# Node ID dd611ab202a8fee088adf1b3303a5197a1fe467e
# Parent  7618e1d9322cccc7c8229ad5caf27287c4a2b480
tweak Metis example to avoid glitch in proof reconstruction with a few guard-based, type-argument-less encodings

diff -r 7618e1d9322c -r dd611ab202a8 src/HOL/Metis_Examples/Type_Encodings.thy
--- a/src/HOL/Metis_Examples/Type_Encodings.thy	Wed Jun 06 10:35:05 2012 +0200
+++ b/src/HOL/Metis_Examples/Type_Encodings.thy	Wed Jun 06 10:35:05 2012 +0200
@@ -27,7 +27,7 @@
    "poly_guards",
    "poly_guards?",
    "poly_guards??",
-   (* "poly_guards@?", *)
+   "poly_guards@?",
    "poly_tags",
    "poly_tags?",
    "poly_tags??",
@@ -73,8 +73,8 @@
 lemma "x = y \<Longrightarrow> y = x"
 by metis_exhaust
 
-lemma "[a] = [1 + 1] \<Longrightarrow> a = 1 + (1::int)"
-by (metis_exhaust last.simps)
+lemma "[a] = [Suc 0] \<Longrightarrow> a = 1"
+by (metis_exhaust last.simps One_nat_def)
 
 lemma "map Suc [0] = [Suc 0]"
 by (metis_exhaust map.simps)
@@ -90,7 +90,7 @@
 lemma "P (null xs) \<Longrightarrow> null xs \<Longrightarrow> xs = []"
 by (metis_exhaust null_def)
 
-lemma "(0::nat) + 0 = 0"
+lemma "(0\<Colon>nat) + 0 = 0"
 by (metis_exhaust add_0_left)
 
 end