1.1 --- a/src/Pure/Isar/proof_context.ML	Tue Mar 09 23:27:35 2010 +0100
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Tue Mar 09 23:29:04 2010 +0100
     1.3 @@ -28,6 +28,7 @@
     1.4    val full_name: Proof.context -> binding -> string
     1.5    val syn_of: Proof.context -> Syntax.syntax
     1.6    val tsig_of: Proof.context -> Type.tsig
     1.7 +  val default_sort: Proof.context -> indexname -> sort
     1.8    val consts_of: Proof.context -> Consts.T
     1.9    val the_const_constraint: Proof.context -> string -> typ
    1.10    val set_syntax_mode: Syntax.mode -> Proof.context -> Proof.context
    1.11 @@ -127,6 +128,9 @@
    1.12      Context.generic -> Context.generic
    1.13    val target_notation: bool -> Syntax.mode -> (term * mixfix) list -> morphism ->
    1.14      Context.generic -> Context.generic
    1.15 +  val class_alias: binding -> class -> Proof.context -> Proof.context
    1.16 +  val type_alias: binding -> string -> Proof.context -> Proof.context
    1.17 +  val const_alias: binding -> string -> Proof.context -> Proof.context
    1.18    val add_const_constraint: string * typ option -> Proof.context -> Proof.context
    1.19    val add_abbrev: string -> binding * term -> Proof.context -> (term * term) * Proof.context
    1.20    val revert_abbrev: string -> string -> Proof.context -> Proof.context
    1.21 @@ -249,6 +253,7 @@
    1.22  val restore_syntax_mode = map_syntax o Local_Syntax.restore_mode o syntax_of;
    1.23  
    1.24  val tsig_of = #1 o #tsigs o rep_context;
    1.25 +fun default_sort ctxt = the_default (Type.defaultS (tsig_of ctxt)) o Variable.def_sort ctxt;
    1.26  
    1.27  val consts_of = #1 o #consts o rep_context;
    1.28  val the_const_constraint = Consts.the_constraint o consts_of;
    1.29 @@ -473,7 +478,7 @@
    1.30    in
    1.31      if Syntax.is_tid c then
    1.32       (Position.report Markup.tfree pos;
    1.33 -      TFree (c, the_default (Type.defaultS tsig) (Variable.def_sort ctxt (c, ~1))))
    1.34 +      TFree (c, default_sort ctxt (c, ~1)))
    1.35      else
    1.36        let
    1.37          val d = Type.intern_type tsig c;
    1.38 @@ -745,7 +750,7 @@
    1.39      val t =
    1.40        Syntax.standard_parse_term (Syntax.pp ctxt) check get_sort map_const map_free
    1.41          ctxt (Type.is_logtype (tsig_of ctxt)) (syn_of ctxt) T' (syms, pos)
    1.42 -      handle ERROR msg => cat_error msg  ("Failed to parse " ^ kind ^ Position.str_of pos);
    1.43 +      handle ERROR msg => cat_error msg ("Failed to parse " ^ kind ^ Position.str_of pos);
    1.44    in t end;
    1.45  
    1.46  
    1.47 @@ -1011,7 +1016,7 @@
    1.48  
    1.49  
    1.50  
    1.51 -(** parameters **)
    1.52 +(** basic logical entities **)
    1.53  
    1.54  (* variables *)
    1.55  
    1.56 @@ -1043,7 +1048,7 @@
    1.57  end;
    1.58  
    1.59  
    1.60 -(* authentic logical entities *)
    1.61 +(* authentic syntax *)
    1.62  
    1.63  val _ = Context.>>
    1.64    (Context.map_theory
    1.65 @@ -1121,8 +1126,14 @@
    1.66        in if Term.aconv_untyped (t, t') then SOME (t', mx) else NONE end);
    1.67    in Context.mapping (Sign.notation add mode args') (notation add mode args') end;
    1.68  
    1.69 +end;
    1.70  
    1.71 -end;
    1.72 +
    1.73 +(* aliases *)
    1.74 +
    1.75 +fun class_alias b c ctxt = (map_tsigs o apfst) (Type.class_alias (naming_of ctxt) b c) ctxt;
    1.76 +fun type_alias b c ctxt = (map_tsigs o apfst) (Type.type_alias (naming_of ctxt) b c) ctxt;
    1.77 +fun const_alias b c ctxt = (map_consts o apfst) (Consts.alias (naming_of ctxt) b c) ctxt;
    1.78  
    1.79  
    1.80  (* local constants *)