| changeset 33519 | e31a85f92ce9 |
| parent 33278 | ba9f52f56356 |
| child 33522 | 737589bb9bb8 |
| 33518:24563731b9b2 | 33519:e31a85f92ce9 |
|---|---|
113 val get_global_hints = #2 o GlobalRecdefData.get; |
113 val get_global_hints = #2 o GlobalRecdefData.get; |
114 |
114 |
115 |
115 |
116 (* proof data *) |
116 (* proof data *) |
117 |
117 |
118 structure LocalRecdefData = ProofDataFun |
118 structure LocalRecdefData = Proof_Data |
119 ( |
119 ( |
120 type T = hints; |
120 type T = hints; |
121 val init = get_global_hints; |
121 val init = get_global_hints; |
122 ); |
122 ); |
123 |
123 |