| changeset 28262 | aa7ca36d67fd |
| parent 26939 | 1035c89b4c02 |
| child 32010 | cb1a1c94b4cd |
| 28261:045187fc7840 | 28262:aa7ca36d67fd |
|---|---|
101 raise Match) |
101 raise Match) |
102 in SOME thm end |
102 in SOME thm end |
103 handle Match => NONE; |
103 handle Match => NONE; |
104 |
104 |
105 |
105 |
106 val conv = Simplifier.simproc @{theory} "data_free" ["(x::i) = y"] proc; |
106 val conv = Simplifier.simproc (the_context ()) "data_free" ["(x::i) = y"] proc; |
107 |
107 |
108 end; |
108 end; |
109 |
109 |
110 |
110 |
111 Addsimprocs [DataFree.conv]; |
111 Addsimprocs [DataFree.conv]; |