1.1 --- a/src/Pure/Isar/proof_context.ML	Mon Feb 15 23:58:24 2010 +0100
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Tue Feb 16 11:27:29 2010 +0100
     1.3 @@ -30,7 +30,6 @@
     1.4    val consts_of: Proof.context -> Consts.T
     1.5    val const_syntax_name: Proof.context -> string -> string
     1.6    val the_const_constraint: Proof.context -> string -> typ
     1.7 -  val mk_const: Proof.context -> string * typ list -> term
     1.8    val set_syntax_mode: Syntax.mode -> Proof.context -> Proof.context
     1.9    val restore_syntax_mode: Proof.context -> Proof.context -> Proof.context
    1.10    val facts_of: Proof.context -> Facts.T
    1.11 @@ -240,8 +239,6 @@
    1.12  val const_syntax_name = Consts.syntax_name o consts_of;
    1.13  val the_const_constraint = Consts.the_constraint o consts_of;
    1.14  
    1.15 -fun mk_const ctxt (c, Ts) = Const (c, Consts.instance (consts_of ctxt) (c, Ts));
    1.16 -
    1.17  val facts_of = #facts o rep_context;
    1.18  val cases_of = #cases o rep_context;
    1.19  
    1.20 @@ -1320,7 +1317,8 @@
    1.21  
    1.22        (*structures*)
    1.23        val structs = Local_Syntax.structs_of (syntax_of ctxt);
    1.24 -      val prt_structs = if null structs then []
    1.25 +      val prt_structs =
    1.26 +        if null structs then []
    1.27          else [Pretty.block (Pretty.str "structures:" :: Pretty.brk 1 ::
    1.28            Pretty.commas (map Pretty.str structs))];
    1.29  
    1.30 @@ -1331,7 +1329,8 @@
    1.31        val fixes =
    1.32          rev (filter_out ((can Name.dest_internal orf member (op =) structs) o #1)
    1.33            (Variable.fixes_of ctxt));
    1.34 -      val prt_fixes = if null fixes then []
    1.35 +      val prt_fixes =
    1.36 +        if null fixes then []
    1.37          else [Pretty.block (Pretty.str "fixed variables:" :: Pretty.brk 1 ::
    1.38            Pretty.commas (map prt_fix fixes))];
    1.39  
    1.40 @@ -1339,7 +1338,8 @@
    1.41        val prems = Assumption.all_prems_of ctxt;
    1.42        val len = length prems;
    1.43        val suppressed = len - ! prems_limit;
    1.44 -      val prt_prems = if null prems then []
    1.45 +      val prt_prems =
    1.46 +        if null prems then []
    1.47          else [Pretty.big_list "prems:" ((if suppressed <= 0 then [] else [Pretty.str "..."]) @
    1.48            map (Display.pretty_thm ctxt) (drop suppressed prems))];
    1.49      in prt_structs @ prt_fixes @ prt_prems end;

     2.1 --- a/src/Pure/ML/ml_antiquote.ML	Mon Feb 15 23:58:24 2010 +0100
     2.2 +++ b/src/Pure/ML/ml_antiquote.ML	Tue Feb 16 11:27:29 2010 +0100
     2.3 @@ -123,9 +123,11 @@
     2.4  val _ = inline "const"
     2.5    (Args.context -- Scan.lift Args.name_source -- Scan.optional
     2.6        (Scan.lift (Args.$$$ "(") |-- OuterParse.enum1' "," Args.typ --| Scan.lift (Args.$$$ ")")) []
     2.7 -    >> (fn ((ctxt, c), Ts) =>
     2.8 -      let val (c, _) = Term.dest_Const (ProofContext.read_const_proper ctxt c)
     2.9 -      in ML_Syntax.atomic (ML_Syntax.print_term (ProofContext.mk_const ctxt (c, Ts))) end));
    2.10 +    >> (fn ((ctxt, raw_c), Ts) =>
    2.11 +      let
    2.12 +        val Const (c, _) = ProofContext.read_const_proper ctxt raw_c;
    2.13 +        val const = Const (c, Consts.instance (ProofContext.consts_of ctxt) (c, Ts));
    2.14 +      in ML_Syntax.atomic (ML_Syntax.print_term const) end));
    2.15  
    2.16  val _ = inline "syntax_const"
    2.17    (Args.context -- Scan.lift Args.name >> (fn (ctxt, c) =>