src/Pure/assumption.ML
changeset 54740 91f54d386680
parent 54567 cfe53047dc16
child 54883 dd04a8b654fc
     1.1 --- a/src/Pure/assumption.ML	Fri Dec 13 14:58:47 2013 +0100
     1.2 +++ b/src/Pure/assumption.ML	Fri Dec 13 20:20:15 2013 +0100
     1.3 @@ -121,6 +121,9 @@
     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 = [], typ = [typ], term = [term], fact = [map thm]} end;
     1.8 +  in
     1.9 +    Morphism.morphism "Assumption.export"
    1.10 +      {binding = [], typ = [typ], term = [term], fact = [map thm]}
    1.11 +  end;
    1.12  
    1.13  end;