src/HOL/Eisbach/method_closure.ML

 end;
 
 structure Method_Closure: METHOD_CLOSURE =
 struct
 
-(* context data *)
+(* context data for ML antiquotation *)
 
 structure Data = Generic_Data
 (
   type T = ((term list * (string list * string list)) * Method.text) Symtab.table;
   val empty: T = Symtab.empty;

       (Symtab.update (Local_Theory.full_name lthy binding,
         (((map (Morphism.term phi) fixes),
           (map (Morphism_name phi) declares, map (Morphism_name phi) methods)),
           (Method.map_source o map) (Token.transform phi) text))));
 
+
+(* context data for method definition *)
 
 structure Local_Data = Proof_Data
 (
   type T =
     (Proof.context -> Method.method) Symtab.table *  (*dynamic methods*)

           val (text, src) = read_closure_input ctxt (Token.input_of tok);
           val _ = Token.assign (SOME (Token.Source src)) tok;
         in text end));
 
 
-fun check_attrib ctxt attrib =
-  let
-    val name = Binding.name_of attrib;
-    val pos = Binding.pos_of attrib;
-    val named_thm = Named_Theorems.check ctxt (name, pos);
-    val parser: Method.modifier parser =
-      Args.$$$ name -- Args.colon >>
-        K {init = I, attribute = Named_Theorems.add named_thm, pos = pos};
-  in (named_thm, parser) end;
-
+(* evaluate method text *)
 
 fun method_evaluate text ctxt =
   let
     val text' =
       text |> (Method.map_source o map o Token.map_facts)

   let
     val morphism = Morphism.term_morphism "method_instantiate" (Envir.norm_term env);
     val text' = (Method.map_source o map) (Token.transform morphism) text;
   in method_evaluate text' end;
 
+
+
+(** Isar command **)
+
+local
+
 fun setup_local_method binding lthy =
   let
     val full_name = Local_Theory.full_name lthy binding;
     fun get_method ctxt = lookup_dynamic_method ctxt full_name ctxt;
   in
     lthy
     |> update_dynamic_method (full_name, K Method.fail)
     |> Method.local_setup binding (Scan.succeed get_method) "(internal)"
   end;
 
+fun check_attrib ctxt attrib =
+  let
+    val name = Binding.name_of attrib;
+    val pos = Binding.pos_of attrib;
+    val named_thm = Named_Theorems.check ctxt (name, pos);
+    val parser: Method.modifier parser =
+      Args.$$$ name -- Args.colon >>
+        K {init = I, attribute = Named_Theorems.add named_thm, pos = pos};
+  in (named_thm, parser) end;
+
 fun dummy_named_thm named_thm =
   Context.proof_map
     (Named_Theorems.clear named_thm
       #> Named_Theorems.add_thm named_thm Drule.free_dummy_thm);
-
-fun parse_method_args method_names =
-  let
-    fun bind_method (name, text) ctxt =
-      let
-        val method = method_evaluate text;
-        val inner_update = method o update_dynamic_method (name, K (method ctxt));
-      in update_dynamic_method (name, inner_update) ctxt end;
-
-    fun rep [] x = Scan.succeed [] x
-      | rep (t :: ts) x = ((method_text >> pair t) ::: rep ts) x;
-  in rep method_names >> fold bind_method end;
-
-
-
-(** Isar command **)
-
-local
 
 fun parse_term_args args =
   Args.context :|-- (fn ctxt =>
     let
       val ctxt' = Proof_Context.set_mode (Proof_Context.mode_schematic) ctxt;

     val tyenv = fold match_types (args ~~ ts) Vartab.empty;
     val tenv =
       fold (fn ((xi, T), t) => Vartab.update_new (xi, (T, t)))
         (map Term.dest_Var args ~~ ts) Vartab.empty;
   in Envir.Envir {maxidx = ~1, tenv = tenv, tyenv = tyenv} end;
+
+fun parse_method_args method_names =
+  let
+    fun bind_method (name, text) ctxt =
+      let
+        val method = method_evaluate text;
+        val inner_update = method o update_dynamic_method (name, K (method ctxt));
+      in update_dynamic_method (name, inner_update) ctxt end;
+
+    fun rep [] x = Scan.succeed [] x
+      | rep (t :: ts) x = ((method_text >> pair t) ::: rep ts) x;
+  in rep method_names >> fold bind_method end;
 
 fun gen_method add_fixes name vars uses declares methods source lthy =
   let
     val (uses_internal, lthy1) = lthy
       |> Proof_Context.concealed