equal
deleted
inserted
replaced
110 let |
110 let |
111 fun dummy_pats (wrap $ (eq $ lhs $ rhs)) = |
111 fun dummy_pats (wrap $ (eq $ lhs $ rhs)) = |
112 let |
112 let |
113 val rhs_vars = Term.add_vars rhs []; |
113 val rhs_vars = Term.add_vars rhs []; |
114 fun dummy (v as Var (ixn as (_, T))) = |
114 fun dummy (v as Var (ixn as (_, T))) = |
115 if member ((=) ) rhs_vars ixn then v else Const (@{const_name DUMMY}, T) |
115 if member ((=) ) rhs_vars ixn then v else Const (\<^const_name>\<open>DUMMY\<close>, T) |
116 | dummy (t $ u) = dummy t $ dummy u |
116 | dummy (t $ u) = dummy t $ dummy u |
117 | dummy (Abs (n, T, b)) = Abs (n, T, dummy b) |
117 | dummy (Abs (n, T, b)) = Abs (n, T, dummy b) |
118 | dummy t = t; |
118 | dummy t = t; |
119 in wrap $ (eq $ dummy lhs $ rhs) end |
119 in wrap $ (eq $ dummy lhs $ rhs) end |
120 in |
120 in |
121 Term_Style.setup @{binding dummy_pats} (Scan.succeed (K dummy_pats)) |
121 Term_Style.setup \<^binding>\<open>dummy_pats\<close> (Scan.succeed (K dummy_pats)) |
122 end |
122 end |
123 \<close> |
123 \<close> |
124 |
124 |
125 setup \<open> |
125 setup \<open> |
126 let |
126 let |
143 in (t'', xs'') end |
143 in (t'', xs'') end |
144 |
144 |
145 val style_eta_expand = |
145 val style_eta_expand = |
146 (Scan.repeat Args.name) >> (fn xs => fn ctxt => fn t => fst (eta_expand [] t xs)) |
146 (Scan.repeat Args.name) >> (fn xs => fn ctxt => fn t => fst (eta_expand [] t xs)) |
147 |
147 |
148 in Term_Style.setup @{binding eta_expand} style_eta_expand end |
148 in Term_Style.setup \<^binding>\<open>eta_expand\<close> style_eta_expand end |
149 \<close> |
149 \<close> |
150 |
150 |
151 end |
151 end |
152 (*>*) |
152 (*>*) |