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;