focus: actually declare constraints for local parameters;
authorwenzelm
Tue Jun 10 16:43:21 2008 +0200 (2008-06-10)
changeset 27119c36c88fcdd22
parent 27118 9a26c0d7a47a
child 27120 b21eec437295
focus: actually declare constraints for local parameters;
src/Pure/variable.ML
     1.1 --- a/src/Pure/variable.ML	Tue Jun 10 16:43:16 2008 +0200
     1.2 +++ b/src/Pure/variable.ML	Tue Jun 10 16:43:21 2008 +0200
     1.3 @@ -468,7 +468,8 @@
     1.4      val (xs', ctxt') = variant_fixes xs ctxt;
     1.5      val ps' = ListPair.map (cert o Free) (xs', Ts);
     1.6      val goal' = fold forall_elim_prop ps' goal;
     1.7 -  in ((ps', goal'), ctxt') end;
     1.8 +    val ctxt'' = ctxt' |> fold (declare_constraints o Thm.term_of) ps';
     1.9 +  in ((ps', goal'), ctxt'') end;
    1.10  
    1.11  fun focus_subgoal i st =
    1.12    let