src/Pure/Isar/element.ML

     else Pretty.keyword1 kind
   in Pretty.block (Pretty.fbreaks (head :: prts)) end;
 
 fun obtain prop ctxt =
   let
-    val ((ps, prop'), ctxt') = Variable.focus prop ctxt;
+    val ((ps, prop'), ctxt') = Variable.focus NONE prop ctxt;
     fun fix (x, T) = (Binding.name (Variable.revert_fixed ctxt' x), SOME T, NoSyn);
     val xs = map (fix o #2) ps;
     val As = Logic.strip_imp_prems prop';
   in ((Binding.empty, (xs, As)), ctxt') end;