# HG changeset patch
# User wenzelm
# Date 1441899150 -7200
# Node ID 82798c8bfa7fb0e31023cb4a903bcf51d1e93481
# Parent  3d5e01b427cb829d1bc1cf553ae37a47922ed5af
removed obsolete undocumented feature;

diff -r 3d5e01b427cb -r 82798c8bfa7f src/Pure/ML/ml_antiquotations.ML
--- a/src/Pure/ML/ml_antiquotations.ML	Thu Sep 10 16:44:17 2015 +0200
+++ b/src/Pure/ML/ml_antiquotations.ML	Thu Sep 10 17:32:30 2015 +0200
@@ -77,12 +77,7 @@
     "Thm.cterm_of ML_context " ^ ML_Syntax.atomic (ML_Syntax.print_term t))) #>
 
   ML_Antiquotation.value @{binding cprop} (Args.prop >> (fn t =>
-    "Thm.cterm_of ML_context " ^ ML_Syntax.atomic (ML_Syntax.print_term t))) #>
-
-  ML_Antiquotation.value @{binding cpat}
-    (Args.context --
-      Scan.lift Args.name_inner_syntax >> uncurry Proof_Context.read_term_pattern >> (fn t =>
-        "Thm.cterm_of ML_context " ^ ML_Syntax.atomic (ML_Syntax.print_term t))));
+    "Thm.cterm_of ML_context " ^ ML_Syntax.atomic (ML_Syntax.print_term t))));
 
 
 (* type classes *)