No resolution of patterns within context statements.
authorballarin
Mon Dec 01 16:59:31 2008 +0100 (2008-12-01)
changeset 28936f1647bf418f5
parent 28927 7e631979922f
child 28937 961c11778778
No resolution of patterns within context statements.
src/FOL/ex/NewLocaleTest.thy
src/Pure/Isar/expression.ML
     1.1 --- a/src/FOL/ex/NewLocaleTest.thy	Mon Dec 01 13:43:32 2008 +0100
     1.2 +++ b/src/FOL/ex/NewLocaleTest.thy	Mon Dec 01 16:59:31 2008 +0100
     1.3 @@ -157,11 +157,6 @@
     1.4    show ?t by (rule x [OF `?a`])
     1.5  qed
     1.6  
     1.7 -lemma
     1.8 -  assumes "P <-> P" (is "?p <-> _")
     1.9 -  shows "?p <-> ?p"
    1.10 -  .
    1.11 -
    1.12  
    1.13  text {* Interpretation between locales: sublocales *}
    1.14  
     2.1 --- a/src/Pure/Isar/expression.ML	Mon Dec 01 13:43:32 2008 +0100
     2.2 +++ b/src/Pure/Isar/expression.ML	Mon Dec 01 16:59:31 2008 +0100
     2.3 @@ -304,12 +304,10 @@
     2.4      (* Type inference *)
     2.5      val (inst_cs' :: css', ctxt') =
     2.6        (fold_burrow o fold_burrow) check (inst_cs :: elem_css @ [concl_cs]) ctxt;
     2.7 -    (* Re-check to resolve bindings, elements and conclusion only *)
     2.8 -    val (css'', _) = (fold_burrow o fold_burrow) check css' ctxt';
     2.9 -    val (elem_css'', [concl_cs'']) = chop (length elem_css) css'';
    2.10 +    val (elem_css', [concl_cs']) = chop (length elem_css) css';
    2.11    in
    2.12 -    (map restore_inst (insts ~~ inst_cs'), map restore_elem (elems ~~ elem_css''),
    2.13 -      concl_cs'', ctxt')
    2.14 +    (map restore_inst (insts ~~ inst_cs'), map restore_elem (elems ~~ elem_css'),
    2.15 +      concl_cs', ctxt')
    2.16    end;
    2.17  
    2.18  end;