diff -r cd28458c2add -r 501491d56798 ProgTutorial/Parsing.thy --- a/ProgTutorial/Parsing.thy Fri Mar 01 00:49:15 2013 +0000 +++ b/ProgTutorial/Parsing.thy Fri Apr 19 11:09:18 2013 +0100 @@ -798,6 +798,7 @@ section {* Parsing Specifications\label{sec:parsingspecs} *} + text {* There are a number of special purpose parsers that help with parsing specifications of function definitions, inductive predicates and so on. In @@ -1512,7 +1513,7 @@ oops method_setup joker = {* - Scan.lift (Scan.succeed (fn ctxt => Method.cheating true ctxt)) *} {* bla *} + Scan.lift (Scan.succeed (fn ctxt => Method.cheating true)) *} {* bla *} lemma "False" apply(joker)