# HG changeset patch
# User wenzelm
# Date 1452010856 -3600
# Node ID 28acb93a745f8dc27fd536d527d838746d5dc353
# Parent  500f54190a3ce38eb7507f9fda03841eaa0ab3ec
unused;

diff -r 500f54190a3c -r 28acb93a745f src/HOL/Eisbach/method_closure.ML
--- a/src/HOL/Eisbach/method_closure.ML	Tue Jan 05 17:14:34 2016 +0100
+++ b/src/HOL/Eisbach/method_closure.ML	Tue Jan 05 17:20:56 2016 +0100
@@ -311,46 +311,4 @@
     fn ctxt => method_instantiate (match fixes) text (setup_ctxt ctxt)
   end;
 
-val _ =
-  Theory.setup
-    (ML_Antiquotation.inline @{binding method}  (* FIXME ML_Antiquotation.value (!?) *)
-      (Args.context -- Scan.lift (Args.mode "drop_cases") -- Scan.lift (Parse.position Parse.name)
-        >> (fn ((ctxt, drop_cases), nameref) =>
-          let
-            val ((targs, (factargs, margs)), _) = get_method ctxt nameref;
-
-            val has_factargs = not (null factargs);
-
-            val (targnms, ctxt') =
-              fold_map (fn (Var ((x, _), _)) => ML_Context.variant x) targs ctxt;
-            val (margnms, ctxt'') = fold_map ML_Context.variant margs ctxt';
-            val (factsnm, _) = ML_Context.variant "facts" ctxt'';
-
-            val fn_header =
-              margnms
-              |> has_factargs ? append [factsnm]
-              |> append targnms
-              |> map (fn nm => "fn " ^ nm ^ " => ")
-              |> implode;
-
-            val ML_context = ML_Context.struct_name ctxt ^ ".ML_context";
-            val ml_inner =
-              ML_Syntax.atomic
-                ("Method_Closure.get_method " ^  ML_context ^
-                  ML_Syntax.print_pair ML_Syntax.print_string ML_Syntax.print_position nameref ^
-                  "|> (fn ((targs, (_, margs)), text) => Method_Closure.eval_method " ^
-                  ML_context ^ " ((targs, margs), text))");
-
-            val drop_cases_suffix =
-              if drop_cases then "#> (fn f => (fn ctxt => fn thms => f ctxt thms |> Seq.map snd))"
-              else "";
-
-            val factsnm = if has_factargs then factsnm else "[]";
-          in
-            ML_Syntax.atomic
-              (fn_header ^ ml_inner ^ " " ^ ML_Syntax.print_list I targnms ^ " " ^
-                factsnm ^ " " ^
-                ML_Syntax.print_list I margnms ^ drop_cases_suffix)
-          end)));
-
 end;