src/HOL/Eisbach/match_method.ML

   Scan.lift (for_fixes -- (@{keyword "\<Rightarrow>"} |-- Parse.token Parse.cartouche))
   >> (fn ((ctxt, ts), (fixes, cartouche)) =>
     (case Token.get_value cartouche of
       SOME (Token.Source src) =>
         let
-          val text = Method_Closure.read_inner_method ctxt src
+          val text = Method_Closure.read ctxt src;
           val ts' =
             map
               (fn (b, (Parse_Tools.Real_Val v, match_args)) =>
                 ((Option.map (fn (b, att) =>
                   (Parse_Tools.the_real_val b, att)) b, match_args), v)
                 | _ => raise Fail "Expected closed term") ts
           val fixes' = map (fn ((p, _), _) => Parse_Tools.the_real_val p) fixes
         in (ts', fixes', text) end
-    | SOME _ => error "Unexpected token value in match cartouche"
-    | NONE =>
+    | _ =>
         let
           val (fix_names, ctxt3) = ctxt
             |> Proof_Context.add_fixes_cmd
               (map (fn ((pb, otyp), _) => (Parse_Tools.the_parse_val pb, otyp, NoSyn)) fixes)
             ||> Proof_Context.set_mode Proof_Context.mode_schematic;

 
           val (binds, ctxt6) = ctxt5
             |> (fn ctxt => fold2 upd_ctxt binds pats ([], ctxt) |> apfst rev)
             ||> Proof_Context.restore_mode ctxt;
 
-          val (src, text) = Method_Closure.read_inner_text_closure ctxt6 (Token.input_of cartouche);
+          val (text, src) = Method_Closure.read_closure_input ctxt6 (Token.input_of cartouche);
 
           val morphism =
             Variable.export_morphism ctxt6
               (ctxt
                 |> fold Token.declare_maxidx src