--- 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)