diff -r 45ab32a542fe -r dd8ec9138112 src/HOL/ex/Cartouche_Examples.thy
--- a/src/HOL/ex/Cartouche_Examples.thy	Sun Nov 30 13:15:04 2014 +0100
+++ b/src/HOL/ex/Cartouche_Examples.thy	Sun Nov 30 14:02:48 2014 +0100
@@ -142,10 +142,7 @@
   Thy_Output.antiquotation @{binding ML_cartouche}
     (Scan.lift Args.cartouche_source_position) (fn {context, ...} => fn source =>
       let
-        val toks =
-          ML_Lex.read Position.none "fn _ => (" @
-          ML_Lex.read_source false source @
-          ML_Lex.read Position.none ");";
+        val toks = ML_Lex.read "fn _ => (" @ ML_Lex.read_source false source @ ML_Lex.read ");";
         val _ = ML_Context.eval_in (SOME context) ML_Compiler.flags (Input.pos_of source) toks;
       in "" end);
 *}
@@ -215,8 +212,7 @@
       val ctxt' = ctxt |> Context.proof_map
         (ML_Context.expression (Input.range_of source) "tactic" "Proof.context -> tactic"
           "Context.map_proof (ML_Tactic.set tactic)"
-          (ML_Lex.read Position.none "fn ctxt: Proof.context =>" @
-           ML_Lex.read_source false source));
+          (ML_Lex.read "fn ctxt: Proof.context =>" @ ML_Lex.read_source false source));
     in Data.get ctxt' ctxt end;
 end;
 *}