# HG changeset patch
# User ballarin
# Date 1228147171 -3600
# Node ID f1647bf418f5eca9abb51c11de6e88c59067e7f2
# Parent  7e631979922fcd9c72790f811ed3091483ca9647
No resolution of patterns within context statements.

diff -r 7e631979922f -r f1647bf418f5 src/FOL/ex/NewLocaleTest.thy
--- a/src/FOL/ex/NewLocaleTest.thy	Mon Dec 01 13:43:32 2008 +0100
+++ b/src/FOL/ex/NewLocaleTest.thy	Mon Dec 01 16:59:31 2008 +0100
@@ -157,11 +157,6 @@
   show ?t by (rule x [OF `?a`])
 qed
 
-lemma
-  assumes "P <-> P" (is "?p <-> _")
-  shows "?p <-> ?p"
-  .
-
 
 text {* Interpretation between locales: sublocales *}
 
diff -r 7e631979922f -r f1647bf418f5 src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Mon Dec 01 13:43:32 2008 +0100
+++ b/src/Pure/Isar/expression.ML	Mon Dec 01 16:59:31 2008 +0100
@@ -304,12 +304,10 @@
     (* Type inference *)
     val (inst_cs' :: css', ctxt') =
       (fold_burrow o fold_burrow) check (inst_cs :: elem_css @ [concl_cs]) ctxt;
-    (* Re-check to resolve bindings, elements and conclusion only *)
-    val (css'', _) = (fold_burrow o fold_burrow) check css' ctxt';
-    val (elem_css'', [concl_cs'']) = chop (length elem_css) css'';
+    val (elem_css', [concl_cs']) = chop (length elem_css) css';
   in
-    (map restore_inst (insts ~~ inst_cs'), map restore_elem (elems ~~ elem_css''),
-      concl_cs'', ctxt')
+    (map restore_inst (insts ~~ inst_cs'), map restore_elem (elems ~~ elem_css'),
+      concl_cs', ctxt')
   end;
 
 end;