| changeset 58963 | 26bf09b95dda |
| parent 58950 | d07464875dd4 |
| child 59058 | a78612c67ec0 |
--- a/src/HOL/Tools/Function/induction_schema.ML Sun Nov 09 20:49:28 2014 +0100 +++ b/src/HOL/Tools/Function/induction_schema.ML Mon Nov 10 21:49:48 2014 +0100 @@ -396,6 +396,6 @@ fun induction_schema_tac ctxt = - mk_ind_tac (K all_tac) (assume_tac APPEND' Goal.assume_rule_tac ctxt) (K all_tac) ctxt; + mk_ind_tac (K all_tac) (assume_tac ctxt APPEND' Goal.assume_rule_tac ctxt) (K all_tac) ctxt; end