src/Pure/Isar/expression.ML
changeset 45289 25e9e7f527b4
parent 43543 eb8b4851b039
child 45290 f599ac41e7f5
     1.1 --- a/src/Pure/Isar/expression.ML	Fri Oct 28 14:10:19 2011 +0200
     1.2 +++ b/src/Pure/Isar/expression.ML	Fri Oct 28 15:38:41 2011 +0200
     1.3 @@ -501,7 +501,8 @@
     1.4      val exp_fact = Drule.zero_var_indexes_list o map Thm.strip_shyps o Morphism.fact export;
     1.5      val exp_term = Term_Subst.zero_var_indexes o Morphism.term export;
     1.6      val exp_typ = Logic.type_map exp_term;
     1.7 -    val export' = Morphism.morphism {binding = I, typ = exp_typ, term = exp_term, fact = exp_fact};
     1.8 +    val export' =
     1.9 +      Morphism.morphism {binding = [], typ = [exp_typ], term = [exp_term], fact = [exp_fact]};
    1.10    in ((propss, deps, export'), goal_ctxt) end;
    1.11  
    1.12  in