--- a/src/Pure/Isar/expression.ML Fri Oct 28 14:10:19 2011 +0200
+++ b/src/Pure/Isar/expression.ML Fri Oct 28 15:38:41 2011 +0200
@@ -501,7 +501,8 @@
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 {binding = I, typ = exp_typ, term = exp_term, fact = exp_fact};
+ val export' =
+ Morphism.morphism {binding = [], typ = [exp_typ], term = [exp_term], fact = [exp_fact]};
in ((propss, deps, export'), goal_ctxt) end;
in