src/Pure/assumption.ML
changeset 28965 1de908189869
parent 26463 9283b4185fdf
child 29579 cb520b766e00
     1.1 --- a/src/Pure/assumption.ML	Wed Dec 03 21:00:39 2008 -0800
     1.2 +++ b/src/Pure/assumption.ML	Thu Dec 04 14:43:33 2008 +0100
     1.3 @@ -120,6 +120,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 {name = I, var = I, typ = typ, term = term, fact = map thm} end;
     1.8 +  in Morphism.morphism {binding = I, var = I, typ = typ, term = term, fact = map thm} end;
     1.9  
    1.10  end;