# HG changeset patch
# User chaieb
# Date 1179591546 -7200
# Node ID a7e23f993c5e00ae0fb14ced4b3d73abc2dad8b0
# Parent  b6cb6a1315114b1e4ab1991975dfee585f47ad19
added cpat antiquotation for reading certified patterns

diff -r b6cb6a131511 -r a7e23f993c5e src/Pure/Thy/ml_context.ML
--- a/src/Pure/Thy/ml_context.ML	Sat May 19 14:05:05 2007 +0200
+++ b/src/Pure/Thy/ml_context.ML	Sat May 19 18:19:06 2007 +0200
@@ -256,6 +256,11 @@
 
 end;
 
+val _ = proj_value_antiq "cpat" (Scan.lift Args.name >> 
+      (fn ns => ("cpat", 
+      "((cterm_of (ML_Context.the_context ())) o Library.the_single o " ^ 
+      "(ProofContext.read_term_pats TypeInfer.logicT (ML_Context.the_local_context ())))"
+      ^ (ML_Syntax.print_list ML_Syntax.print_string [ns]), "")));
 
 (*final declarations of this structure!*)
 nonfix >>;