| changeset 59058 | a78612c67ec0 |
| parent 58821 | 11e226e8a095 |
| child 59498 | 50b60f501b05 |
--- a/src/HOL/Tools/Transfer/transfer.ML Wed Nov 26 16:55:43 2014 +0100 +++ b/src/HOL/Tools/Transfer/transfer.ML Wed Nov 26 20:05:34 2014 +0100 @@ -48,7 +48,7 @@ (** Theory Data **) -val compound_xhs_empty_net = Item_Net.init (Thm.eq_thm_prop o pairself snd) (single o fst); +val compound_xhs_empty_net = Item_Net.init (Thm.eq_thm_prop o apply2 snd) (single o fst); val rewr_rules = Item_Net.init Thm.eq_thm_prop (single o fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.concl_of);