| changeset 42814 | 5af15f1e2ef6 |
| parent 42802 | 51d7e74f6899 |
| child 43560 | d1650e3720fd |
--- a/src/FOL/FOL.thy Sun May 15 17:06:35 2011 +0200 +++ b/src/FOL/FOL.thy Sun May 15 17:45:53 2011 +0200 @@ -73,7 +73,7 @@ method_setup case_tac = {* Args.goal_spec -- Scan.lift Args.name_source >> - (fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (case_tac ctxt s)) + (fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (case_tac ctxt s)) *} "case_tac emulation (dynamic instantiation!)"