author | wenzelm |
Sat, 29 Oct 2011 00:23:58 +0200 | |
changeset 45295 | 255200892a42 |
parent 45294 | 3c5d3d286055 |
child 45296 | 7a97b2bda137 |
--- a/src/Pure/Isar/element.ML Fri Oct 28 23:41:16 2011 +0200 +++ b/src/Pure/Isar/element.ML Sat Oct 29 00:23:58 2011 +0200 @@ -397,7 +397,7 @@ fun instT_morphism thy env = let val thy_ref = Theory.check_thy thy in Morphism.morphism - {binding = [I], + {binding = [], typ = [instT_type env], term = [instT_term env], fact = [map (fn th => instT_thm (Theory.deref thy_ref) env th)]}