# HG changeset patch
# User wenzelm
# Date 1190579017 -7200
# Node ID c3d56f41483bc1e70f9ee664cad2498e5515b685
# Parent  80da599dea376fc619f56d563e0d9dbe7667e308
tuned @{cpat};

diff -r 80da599dea37 -r c3d56f41483b src/Pure/ML/ml_context.ML
--- a/src/Pure/ML/ml_context.ML	Sun Sep 23 22:23:35 2007 +0200
+++ b/src/Pure/ML/ml_context.ML	Sun Sep 23 22:23:37 2007 +0200
@@ -257,11 +257,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]), "")));
+val _ = proj_value_antiq "cpat" (Scan.lift Args.name >>
+    (fn name => ("cpat",
+      "Thm.cterm_of (ML_Context.the_context ()) (Syntax.read_term \
+      \(ProofContext.set_mode ProofContext.mode_pattern (ML_Context.the_local_context ()))"
+      ^ ML_Syntax.print_string name ^ ")", "")));
 
 (*final declarations of this structure!*)
 nonfix >>;