src/HOL/Import/replay.ML
changeset 29585 c23295521af5
parent 28662 64ab5bb68d4c
child 30346 90efbb8a8cb2
     1.1 --- a/src/HOL/Import/replay.ML	Wed Jan 21 16:51:45 2009 +0100
     1.2 +++ b/src/HOL/Import/replay.ML	Wed Jan 21 18:27:43 2009 +0100
     1.3 @@ -340,7 +340,7 @@
     1.4  	  | delta (Hol_move (fullname, moved_thmname)) thy = 
     1.5  	    add_hol4_move fullname moved_thmname thy
     1.6  	  | delta (Defs (thmname, eq)) thy =
     1.7 -	    snd (PureThy.add_defs false [((thmname, eq), [])] thy)
     1.8 +	    snd (PureThy.add_defs false [((Binding.name thmname, eq), [])] thy)
     1.9  	  | delta (Hol_theorem (thyname, thmname, th)) thy =
    1.10  	    add_hol4_theorem thyname thmname ([], th_of thy th) thy
    1.11  	  | delta (Typedef (thmname, typ, c, repabs, th)) thy =