122 |
122 |
123 (*Strips assumptions in goal yielding ( [x1,...,xm], [H1,...,Hn], B ) |
123 (*Strips assumptions in goal yielding ( [x1,...,xm], [H1,...,Hn], B ) |
124 H1,...,Hn are the hypotheses; x1...xm are variants of the parameters. |
124 H1,...,Hn are the hypotheses; x1...xm are variants of the parameters. |
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 (\<^const_name>\<open>Pure.imp\<close>, _) $ H $ B) = |
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 (\<^const_name>\<open>Pure.all\<close>,_) $ Abs (a, T, t)) = |
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) = Syntax_Trans.variant_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); |