# HG changeset patch
# User ballarin
# Date 1228149497 -3600
# Node ID 32542abe665656daaf3018350e12efa9a629cdf3
# Parent  961c11778778691a7015ab90b13be54acaa6de51# Parent  6c9d81544b260e9408735382b22bde0c2b16303a
Merged again.

diff -r 6c9d81544b26 -r 32542abe6656 src/FOL/ex/NewLocaleTest.thy
--- a/src/FOL/ex/NewLocaleTest.thy	Mon Dec 01 17:32:40 2008 +0100
+++ b/src/FOL/ex/NewLocaleTest.thy	Mon Dec 01 17:38:17 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 6c9d81544b26 -r 32542abe6656 src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Mon Dec 01 17:32:40 2008 +0100
+++ b/src/Pure/Isar/expression.ML	Mon Dec 01 17:38:17 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;