--- 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 >>;