# HG changeset patch
# User wenzelm
# Date 1206374974 -3600
# Node ID be47e9a83b4f8a2a7bf0d601fd6055ee2fd05da6
# Parent  b615c10404bf82447f74303e65f6845920050e91
simplified thm_antiq;

diff -r b615c10404bf -r be47e9a83b4f src/Pure/ML/ml_context.ML
--- a/src/Pure/ML/ml_context.ML	Mon Mar 24 17:09:33 2008 +0100
+++ b/src/Pure/ML/ml_context.ML	Mon Mar 24 17:09:34 2008 +0100
@@ -275,19 +275,16 @@
   | print_interval (Facts.From i) = "Facts.From " ^ ML_Syntax.print_int i
   | print_interval (Facts.Single i) = "Facts.Single " ^ ML_Syntax.print_int i;
 
-fun print_named args =
-  "Facts.Named " ^
-    ML_Syntax.print_pair (ML_Syntax.print_pair ML_Syntax.print_string ML_Syntax.print_position)
-      (ML_Syntax.print_option (ML_Syntax.print_list print_interval)) args;
-
 fun thm_antiq kind get get_name = value_antiq kind
   ((Scan.state >> Context.proof_of) --
     Scan.lift (Args.position Args.name -- Scan.option Args.thm_sel)
-  >> (fn (ctxt, thmspec as ((name, _), _)) =>
+  >> (fn (ctxt, ((name, pos), sel)) =>
       let
-        val _ = get ctxt (Facts.Named thmspec);
-        val thmspec_txt = ML_Syntax.atomic (print_named thmspec);
-      in (name, get_name ^ " (ML_Context.the_local_context ()) " ^ thmspec_txt) end));
+        val _ = get ctxt (Facts.Named ((name, pos), sel));
+        val txt =
+          "(Facts.Named ((" ^ ML_Syntax.print_string name ^ ", Position.none), " ^
+            ML_Syntax.print_option (ML_Syntax.print_list print_interval) sel ^ "))";
+      in (name, get_name ^ " (ML_Context.the_local_context ()) " ^ txt) end));
 
 in