# HG changeset patch
# User wenzelm
# Date 975696125 -3600
# Node ID e7c9900cca4d8649b87796fac93490a62456b145
# Parent  7ed4f5a6c63f28a0c23147dd7f8b4a3ee6dbc6ca
schematic goals;

diff -r 7ed4f5a6c63f -r e7c9900cca4d src/HOL/Lambda/Type.thy
--- a/src/HOL/Lambda/Type.thy	Fri Dec 01 19:41:45 2000 +0100
+++ b/src/HOL/Lambda/Type.thy	Fri Dec 01 19:42:05 2000 +0100
@@ -59,16 +59,12 @@
 
 subsection {* Some examples *}
 
-lemma "\<exists>T U. e |- Abs (Abs (Abs (Var 1 $ (Var 2 $ Var 1 $ Var 0)))) : T \<and> U = T"
-  apply (intro exI conjI)
-   apply force
-  apply (rule refl)
+lemma "e |- Abs (Abs (Abs (Var 1 $ (Var 2 $ Var 1 $ Var 0)))) : ?T"
+  apply force
   done
 
-lemma "\<exists>T U. e |- Abs (Abs (Abs (Var 2 $ Var 0 $ (Var 1 $ Var 0)))) : T \<and> U = T";
-  apply (intro exI conjI)
-   apply force
-  apply (rule refl)
+lemma "e |- Abs (Abs (Abs (Var 2 $ Var 0 $ (Var 1 $ Var 0)))) : ?T"
+  apply force
   done