src/Pure/Isar/expression.ML
changeset 28936 f1647bf418f5
parent 28903 b3fc3a62247a
child 28951 e89dde5f365c
--- 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;