# HG changeset patch
# User wenzelm
# Date 1268173744 -3600
# Node ID 8977403824421bbd9d796c95d37bba04ccf11ce5
# Parent  da87ffdcf7eae73aca0d2547bb8d5eed55030501
aliases for class/type/const;
tuned;

diff -r da87ffdcf7ea -r 897740382442 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Tue Mar 09 23:27:35 2010 +0100
+++ b/src/Pure/Isar/proof_context.ML	Tue Mar 09 23:29:04 2010 +0100
@@ -28,6 +28,7 @@
   val full_name: Proof.context -> binding -> string
   val syn_of: Proof.context -> Syntax.syntax
   val tsig_of: Proof.context -> Type.tsig
+  val default_sort: Proof.context -> indexname -> sort
   val consts_of: Proof.context -> Consts.T
   val the_const_constraint: Proof.context -> string -> typ
   val set_syntax_mode: Syntax.mode -> Proof.context -> Proof.context
@@ -127,6 +128,9 @@
     Context.generic -> Context.generic
   val target_notation: bool -> Syntax.mode -> (term * mixfix) list -> morphism ->
     Context.generic -> Context.generic
+  val class_alias: binding -> class -> Proof.context -> Proof.context
+  val type_alias: binding -> string -> Proof.context -> Proof.context
+  val const_alias: binding -> string -> Proof.context -> Proof.context
   val add_const_constraint: string * typ option -> Proof.context -> Proof.context
   val add_abbrev: string -> binding * term -> Proof.context -> (term * term) * Proof.context
   val revert_abbrev: string -> string -> Proof.context -> Proof.context
@@ -249,6 +253,7 @@
 val restore_syntax_mode = map_syntax o Local_Syntax.restore_mode o syntax_of;
 
 val tsig_of = #1 o #tsigs o rep_context;
+fun default_sort ctxt = the_default (Type.defaultS (tsig_of ctxt)) o Variable.def_sort ctxt;
 
 val consts_of = #1 o #consts o rep_context;
 val the_const_constraint = Consts.the_constraint o consts_of;
@@ -473,7 +478,7 @@
   in
     if Syntax.is_tid c then
      (Position.report Markup.tfree pos;
-      TFree (c, the_default (Type.defaultS tsig) (Variable.def_sort ctxt (c, ~1))))
+      TFree (c, default_sort ctxt (c, ~1)))
     else
       let
         val d = Type.intern_type tsig c;
@@ -745,7 +750,7 @@
     val t =
       Syntax.standard_parse_term (Syntax.pp ctxt) check get_sort map_const map_free
         ctxt (Type.is_logtype (tsig_of ctxt)) (syn_of ctxt) T' (syms, pos)
-      handle ERROR msg => cat_error msg  ("Failed to parse " ^ kind ^ Position.str_of pos);
+      handle ERROR msg => cat_error msg ("Failed to parse " ^ kind ^ Position.str_of pos);
   in t end;
 
 
@@ -1011,7 +1016,7 @@
 
 
 
-(** parameters **)
+(** basic logical entities **)
 
 (* variables *)
 
@@ -1043,7 +1048,7 @@
 end;
 
 
-(* authentic logical entities *)
+(* authentic syntax *)
 
 val _ = Context.>>
   (Context.map_theory
@@ -1121,8 +1126,14 @@
       in if Term.aconv_untyped (t, t') then SOME (t', mx) else NONE end);
   in Context.mapping (Sign.notation add mode args') (notation add mode args') end;
 
+end;
 
-end;
+
+(* aliases *)
+
+fun class_alias b c ctxt = (map_tsigs o apfst) (Type.class_alias (naming_of ctxt) b c) ctxt;
+fun type_alias b c ctxt = (map_tsigs o apfst) (Type.type_alias (naming_of ctxt) b c) ctxt;
+fun const_alias b c ctxt = (map_consts o apfst) (Consts.alias (naming_of ctxt) b c) ctxt;
 
 
 (* local constants *)
diff -r da87ffdcf7ea -r 897740382442 src/Pure/consts.ML
--- a/src/Pure/consts.ML	Tue Mar 09 23:27:35 2010 +0100
+++ b/src/Pure/consts.ML	Tue Mar 09 23:29:04 2010 +0100
@@ -19,6 +19,7 @@
   val is_monomorphic: T -> string -> bool                      (*exception TYPE*)
   val the_constraint: T -> string -> typ                       (*exception TYPE*)
   val space_of: T -> Name_Space.T
+  val alias: Name_Space.naming -> binding -> string -> T -> T
   val is_concealed: T -> string -> bool
   val intern: T -> xstring -> string
   val extern: T -> string -> xstring
@@ -122,6 +123,9 @@
 
 fun space_of (Consts {decls = (space, _), ...}) = space;
 
+fun alias naming binding name = map_consts (fn ((space, decls), constraints, rev_abbrevs) =>
+  ((Name_Space.alias naming binding name space, decls), constraints, rev_abbrevs));
+
 val is_concealed = Name_Space.is_concealed o space_of;
 
 val intern = Name_Space.intern o space_of;
diff -r da87ffdcf7ea -r 897740382442 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Tue Mar 09 23:27:35 2010 +0100
+++ b/src/Pure/sign.ML	Tue Mar 09 23:29:04 2010 +0100
@@ -47,6 +47,9 @@
   val class_space: theory -> Name_Space.T
   val type_space: theory -> Name_Space.T
   val const_space: theory -> Name_Space.T
+  val class_alias: binding -> class -> theory -> theory
+  val type_alias: binding -> string -> theory -> theory
+  val const_alias: binding -> string -> theory -> theory
   val intern_class: theory -> xstring -> string
   val extern_class: theory -> string -> xstring
   val intern_type: theory -> xstring -> string
@@ -233,6 +236,10 @@
 val type_space = Type.type_space o tsig_of;
 val const_space = Consts.space_of o consts_of;
 
+fun class_alias b c thy = map_tsig (Type.class_alias (naming_of thy) b c) thy;
+fun type_alias b c thy = map_tsig (Type.type_alias (naming_of thy) b c) thy;
+fun const_alias b c thy = map_consts (Consts.alias (naming_of thy) b c) thy;
+
 val intern_class = Name_Space.intern o class_space;
 val extern_class = Name_Space.extern o class_space;
 val intern_type = Name_Space.intern o type_space;
diff -r da87ffdcf7ea -r 897740382442 src/Pure/type.ML
--- a/src/Pure/type.ML	Tue Mar 09 23:27:35 2010 +0100
+++ b/src/Pure/type.ML	Tue Mar 09 23:29:04 2010 +0100
@@ -21,6 +21,7 @@
     log_types: string list}
   val empty_tsig: tsig
   val class_space: tsig -> Name_Space.T
+  val class_alias: Name_Space.naming -> binding -> string -> tsig -> tsig
   val intern_class: tsig -> xstring -> string
   val extern_class: tsig -> string -> xstring
   val defaultS: tsig -> sort
@@ -40,6 +41,7 @@
   val set_mode: mode -> Proof.context -> Proof.context
   val restore_mode: Proof.context -> Proof.context -> Proof.context
   val type_space: tsig -> Name_Space.T
+  val type_alias: Name_Space.naming -> binding -> string -> tsig -> tsig
   val intern_type: tsig -> xstring -> string
   val extern_type: tsig -> string -> xstring
   val is_logtype: tsig -> string -> bool
@@ -141,6 +143,9 @@
 
 val class_space = #1 o #classes o rep_tsig;
 
+fun class_alias naming binding name = map_tsig (fn ((space, classes), default, types) =>
+  ((Name_Space.alias naming binding name space, classes), default, types));
+
 val intern_class = Name_Space.intern o class_space;
 val extern_class = Name_Space.extern o class_space;
 
@@ -182,6 +187,9 @@
 
 val type_space = #1 o #types o rep_tsig;
 
+fun type_alias naming binding name = map_tsig (fn (classes, default, (space, types)) =>
+  (classes, default, (Name_Space.alias naming binding name space, types)));
+
 val intern_type = Name_Space.intern o type_space;
 val extern_type = Name_Space.extern o type_space;