diff -r 1dc3514c1719 -r 9cb269b49cf7 src/HOL/Tools/Metis/metis_reconstruct.ML
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Wed Aug 07 18:23:32 2019 +0200
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Thu Aug 08 10:50:23 2019 +0200
@@ -300,7 +300,7 @@
 
 val REFL_THM = Thm.incr_indexes 2 @{lemma "t \<noteq> t \<Longrightarrow> False" by (drule notE) (rule refl)}
 
-val refl_x = Thm.cterm_of \<^context> (Var (hd (Term.add_vars (Thm.prop_of REFL_THM) [])));
+val [refl_x] = Term.add_vars (Thm.prop_of REFL_THM) [];
 val refl_idx = 1 + Thm.maxidx_of REFL_THM;
 
 fun refl_inference ctxt type_enc concealed sym_tab t =
@@ -308,7 +308,7 @@
     val i_t = singleton (hol_terms_of_metis ctxt type_enc concealed sym_tab) t
     val _ = trace_msg ctxt (fn () => "  term: " ^ Syntax.string_of_term ctxt i_t)
     val c_t = cterm_incr_types ctxt refl_idx i_t
-  in infer_instantiate_types ctxt [(dest_Var (Thm.term_of refl_x), c_t)] REFL_THM end
+  in infer_instantiate_types ctxt [(refl_x, c_t)] REFL_THM end
 
 (* INFERENCE RULE: EQUALITY *)