src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML
changeset 57954 c52223cd1003
parent 57945 cacb00a569e0
child 59498 50b60f501b05
     1.1 --- a/src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML	Sat Aug 16 14:42:35 2014 +0200
     1.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML	Sat Aug 16 16:18:39 2014 +0200
     1.3 @@ -131,11 +131,11 @@
     1.4  
     1.5  val get_rec_tab = Rec_Data.get
     1.6  fun get_deflation_thms thy =
     1.7 -  Named_Theorems.get (Proof_Context.init_global thy) @{named_theorems domain_deflation}
     1.8 +  rev (Named_Theorems.get (Proof_Context.init_global thy) @{named_theorems domain_deflation})
     1.9  
    1.10  val map_ID_add = Named_Theorems.add @{named_theorems domain_map_ID}
    1.11  fun get_map_ID_thms thy =
    1.12 -  Named_Theorems.get (Proof_Context.init_global thy) @{named_theorems domain_map_ID}
    1.13 +  rev (Named_Theorems.get (Proof_Context.init_global thy) @{named_theorems domain_map_ID})
    1.14  
    1.15  
    1.16  (******************************************************************************)