src/Pure/variable.ML

     val ps = Term.variant_frees t (Term.strip_all_vars t);   (*as they are printed :-*)
     val (xs, Ts) = split_list ps;
     val (xs', ctxt') = variant_fixes xs ctxt;
     val ps' = ListPair.map (cert o Free) (xs', Ts);
     val goal' = fold forall_elim_prop ps' goal;
-  in ((ps', goal'), ctxt') end;
+    val ctxt'' = ctxt' |> fold (declare_constraints o Thm.term_of) ps';
+  in ((ps', goal'), ctxt'') end;
 
 fun focus_subgoal i st =
   let
     val all_vars = Thm.fold_terms Term.add_vars st [];
     val no_binds = map (fn (xi, _) => (xi, NONE)) all_vars;