src/Pure/Isar/element.ML

 fun obtain prop ctxt =
   let
     val ((xs, prop'), ctxt') = Variable.focus prop ctxt;
     val As = Logic.strip_imp_prems (Thm.term_of prop');
     fun var (x, T) = (ProofContext.revert_skolem ctxt' x, SOME T);
-  in (("", (map var xs, As)), ctxt') end;
+  in (("", (map (var o Term.dest_Free o Thm.term_of) xs, As)), ctxt') end;
 
 in
 
 fun pretty_statement ctxt kind raw_th =
   let

     val cert = Thm.cterm_of thy;
 
     val th = Goal.norm_hhf raw_th;
     val is_elim = ObjectLogic.is_elim th;
 
-    val ([th'], ctxt') = Variable.import true [th] ctxt;
+    val ((_, [th']), ctxt') = Variable.import true [th] ctxt;
     val prop = Thm.prop_of th';
     val (prems, concl) = Logic.strip_horn prop;
     val concl_term = ObjectLogic.drop_judgment thy concl;
 
     val fixes = fold_aterms (fn v as Free (x, T) =>