# HG changeset patch
# User blanchet
# Date 1305907932 -7200
# Node ID d96e53d0c638709fd5ae40a4a454f79d678f3ed8
# Parent  c8d9bce88f89d7ab6901e74576283ff34b5796d4
update example

diff -r c8d9bce88f89 -r d96e53d0c638 src/HOL/Metis_Examples/HO_Reas.thy
--- a/src/HOL/Metis_Examples/HO_Reas.thy	Fri May 20 18:01:46 2011 +0200
+++ b/src/HOL/Metis_Examples/HO_Reas.thy	Fri May 20 18:12:12 2011 +0200
@@ -56,7 +56,7 @@
 
 lemma "id (op =) x x"
 sledgehammer [type_sys = erased, expect = none] (id_apply)
-sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
+sledgehammer [type_sys = poly_tags?, expect = none] (id_apply) (* unfortunate *)
 sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
 sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
 sledgehammer [type_sys = poly_preds, expect = some] (id_apply)