src/Pure/assumption.ML
changeset 45289 25e9e7f527b4
parent 41552 c5e71fee3617
child 45650 d314a4e8038f
     1.1 --- a/src/Pure/assumption.ML	Fri Oct 28 14:10:19 2011 +0200
     1.2 +++ b/src/Pure/assumption.ML	Fri Oct 28 15:38:41 2011 +0200
     1.3 @@ -124,6 +124,6 @@
     1.4      val thm = export false inner outer;
     1.5      val term = export_term inner outer;
     1.6      val typ = Logic.type_map term;
     1.7 -  in Morphism.morphism {binding = I, typ = typ, term = term, fact = map thm} end;
     1.8 +  in Morphism.morphism {binding = [], typ = [typ], term = [term], fact = [map thm]} end;
     1.9  
    1.10  end;