125 Main difference from strip_assums concerns parameters: |
125 Main difference from strip_assums concerns parameters: |
126 it replaces the bound variables by free variables. *) |
126 it replaces the bound variables by free variables. *) |
127 fun strip_context_aux (params, Hs, \<^Const_>\<open>Pure.imp for H B\<close>) = |
127 fun strip_context_aux (params, Hs, \<^Const_>\<open>Pure.imp for H B\<close>) = |
128 strip_context_aux (params, H :: Hs, B) |
128 strip_context_aux (params, H :: Hs, B) |
129 | strip_context_aux (params, Hs, \<^Const_>\<open>Pure.all _ for \<open>Abs (a, T, t)\<close>\<close>) = |
129 | strip_context_aux (params, Hs, \<^Const_>\<open>Pure.all _ for \<open>Abs (a, T, t)\<close>\<close>) = |
130 let val (b, u) = Syntax_Trans.variant_abs (a, T, t) |
130 let val (b, u) = Term.dest_abs (a, T, t) |
131 in strip_context_aux ((b, T) :: params, Hs, u) end |
131 in strip_context_aux ((b, T) :: params, Hs, u) end |
132 | strip_context_aux (params, Hs, B) = (rev params, rev Hs, B); |
132 | strip_context_aux (params, Hs, B) = (rev params, rev Hs, B); |
133 |
133 |
134 fun strip_context A = strip_context_aux ([], [], A); |
134 fun strip_context A = strip_context_aux ([], [], A); |
135 |
135 |