src/Pure/assumption.ML
changeset 29605 f2924219125e
parent 29579 cb520b766e00
child 30471 178de3995e91
     1.1 --- a/src/Pure/assumption.ML	Wed Jan 21 22:26:49 2009 +0100
     1.2 +++ b/src/Pure/assumption.ML	Wed Jan 21 22:26:49 2009 +0100
     1.3 @@ -119,6 +119,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, var = I, typ = typ, term = term, fact = map thm} end;
     1.8 +  in Morphism.morphism {binding = I, typ = typ, term = term, fact = map thm} end;
     1.9  
    1.10  end;