| changeset 56722 | ba1ac087b3a7 |
| parent 56524 | f4ba736040fa |
| child 58821 | 11e226e8a095 |
--- a/src/HOL/Tools/Transfer/transfer.ML Fri Apr 25 14:39:11 2014 +0200 +++ b/src/HOL/Tools/Transfer/transfer.ML Fri Apr 25 17:54:54 2014 +0200 @@ -55,7 +55,7 @@ type pred_data = {rel_eq_onp: thm} -val rel_eq_onp = #rel_eq_onp +val rel_eq_onp: pred_data -> thm = #rel_eq_onp structure Data = Generic_Data (