# HG changeset patch
# User wenzelm
# Date 1266316049 -3600
# Node ID e1a226a191b60164b97eafa9a29c1d1bb059f72c
# Parent  ad213c602ec113c91a7ee2918893734b1d49f86b
misc tuning and simplification;

diff -r ad213c602ec1 -r e1a226a191b6 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Mon Feb 15 23:58:24 2010 +0100
+++ b/src/Pure/Isar/proof_context.ML	Tue Feb 16 11:27:29 2010 +0100
@@ -30,7 +30,6 @@
   val consts_of: Proof.context -> Consts.T
   val const_syntax_name: Proof.context -> string -> string
   val the_const_constraint: Proof.context -> string -> typ
-  val mk_const: Proof.context -> string * typ list -> term
   val set_syntax_mode: Syntax.mode -> Proof.context -> Proof.context
   val restore_syntax_mode: Proof.context -> Proof.context -> Proof.context
   val facts_of: Proof.context -> Facts.T
@@ -240,8 +239,6 @@
 val const_syntax_name = Consts.syntax_name o consts_of;
 val the_const_constraint = Consts.the_constraint o consts_of;
 
-fun mk_const ctxt (c, Ts) = Const (c, Consts.instance (consts_of ctxt) (c, Ts));
-
 val facts_of = #facts o rep_context;
 val cases_of = #cases o rep_context;
 
@@ -1320,7 +1317,8 @@
 
       (*structures*)
       val structs = Local_Syntax.structs_of (syntax_of ctxt);
-      val prt_structs = if null structs then []
+      val prt_structs =
+        if null structs then []
         else [Pretty.block (Pretty.str "structures:" :: Pretty.brk 1 ::
           Pretty.commas (map Pretty.str structs))];
 
@@ -1331,7 +1329,8 @@
       val fixes =
         rev (filter_out ((can Name.dest_internal orf member (op =) structs) o #1)
           (Variable.fixes_of ctxt));
-      val prt_fixes = if null fixes then []
+      val prt_fixes =
+        if null fixes then []
         else [Pretty.block (Pretty.str "fixed variables:" :: Pretty.brk 1 ::
           Pretty.commas (map prt_fix fixes))];
 
@@ -1339,7 +1338,8 @@
       val prems = Assumption.all_prems_of ctxt;
       val len = length prems;
       val suppressed = len - ! prems_limit;
-      val prt_prems = if null prems then []
+      val prt_prems =
+        if null prems then []
         else [Pretty.big_list "prems:" ((if suppressed <= 0 then [] else [Pretty.str "..."]) @
           map (Display.pretty_thm ctxt) (drop suppressed prems))];
     in prt_structs @ prt_fixes @ prt_prems end;
diff -r ad213c602ec1 -r e1a226a191b6 src/Pure/ML/ml_antiquote.ML
--- a/src/Pure/ML/ml_antiquote.ML	Mon Feb 15 23:58:24 2010 +0100
+++ b/src/Pure/ML/ml_antiquote.ML	Tue Feb 16 11:27:29 2010 +0100
@@ -123,9 +123,11 @@
 val _ = inline "const"
   (Args.context -- Scan.lift Args.name_source -- Scan.optional
       (Scan.lift (Args.$$$ "(") |-- OuterParse.enum1' "," Args.typ --| Scan.lift (Args.$$$ ")")) []
-    >> (fn ((ctxt, c), Ts) =>
-      let val (c, _) = Term.dest_Const (ProofContext.read_const_proper ctxt c)
-      in ML_Syntax.atomic (ML_Syntax.print_term (ProofContext.mk_const ctxt (c, Ts))) end));
+    >> (fn ((ctxt, raw_c), Ts) =>
+      let
+        val Const (c, _) = ProofContext.read_const_proper ctxt raw_c;
+        val const = Const (c, Consts.instance (ProofContext.consts_of ctxt) (c, Ts));
+      in ML_Syntax.atomic (ML_Syntax.print_term const) end));
 
 val _ = inline "syntax_const"
   (Args.context -- Scan.lift Args.name >> (fn (ctxt, c) =>