src/Pure/Isar/expression.ML

     val exp_fact = Drule.zero_var_indexes_list o map Thm.strip_shyps o Morphism.fact export;
     val exp_term = Term_Subst.zero_var_indexes o Morphism.term export;
     val exp_typ = Logic.type_map exp_term;
     val export' =
       Morphism.morphism "Expression.prep_goal"
-        {binding = [], typ = [exp_typ], term = [exp_term], fact = [exp_fact]};
+        {binding = [], typ = [K exp_typ], term = [K exp_term], fact = [K exp_fact]};
   in ((propss, eq_propss, deps, eqnss, export'), goal_ctxt) end;
 
 in
 
 fun cert_goal_expression x = prep_goal_expression cert_full_context_statement x;