changeset 61912 | ad710de5c576 |
parent 61911 | fe2b7f4276be |
child 61917 | 35ec3757d3c1 |
--- a/src/HOL/Eisbach/method_closure.ML Tue Dec 22 17:14:35 2015 +0100 +++ b/src/HOL/Eisbach/method_closure.ML Tue Dec 22 17:41:46 2015 +0100 @@ -90,7 +90,7 @@ val method_text = - Args.context -- Scan.lift (Parse.token Parse.cartouche) >> (fn (ctxt, tok) => + Args.context -- Scan.lift (Parse.token Parse.text) >> (fn (ctxt, tok) => (case Token.get_value tok of SOME (Token.Source src) => read ctxt src | _ =>