localized default sort;

--- a/src/Pure/Isar/isar_syn.ML	Wed Apr 28 11:13:11 2010 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Wed Apr 28 11:41:27 2010 +0200
@@ -96,9 +96,9 @@
     >> (Toplevel.theory o AxClass.axiomatize_classrel_cmd));
 
 val _ =
-  OuterSyntax.command "defaultsort" "declare default sort" K.thy_decl
-    (P.sort >>
-      (fn s => Toplevel.theory (fn thy => Sign.set_defsort (Syntax.read_sort_global thy s) thy)));
+  OuterSyntax.local_theory "defaultsort" "declare default sort for explicit type variables"
+    K.thy_decl
+    (P.sort >> (fn s => fn lthy => Local_Theory.set_defsort (Syntax.read_sort lthy s) lthy));
 
 
 (* types *)

--- a/src/Pure/Isar/local_theory.ML	Wed Apr 28 11:13:11 2010 +0200
+++ b/src/Pure/Isar/local_theory.ML	Wed Apr 28 11:41:27 2010 +0200
@@ -40,6 +40,7 @@
     local_theory -> (string * thm list) list * local_theory
   val declaration: bool -> declaration -> local_theory -> local_theory
   val syntax_declaration: bool -> declaration -> local_theory -> local_theory
+  val set_defsort: sort -> local_theory -> local_theory
   val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> local_theory -> local_theory
   val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
   val class_alias: binding -> class -> local_theory -> local_theory
@@ -183,7 +184,7 @@
 fun global_morphism lthy = standard_morphism lthy (ProofContext.init (ProofContext.theory_of lthy));
 
 
-(* basic operations *)
+(* primitive operations *)
 
 fun operation f lthy = f (#operations (get_lthy lthy)) lthy;
 fun operation1 f x = operation (fn ops => f ops x);
@@ -196,9 +197,16 @@
 val declaration = checkpoint ooo operation2 #declaration;
 val syntax_declaration = checkpoint ooo operation2 #syntax_declaration;
 
+
+
+(** basic derived operations **)
+
 val notes = notes_kind "";
 fun note (a, ths) = notes [(a, [(ths, [])])] #>> the_single;
 
+fun set_defsort S =
+  syntax_declaration false (K (Context.mapping (Sign.set_defsort S) (ProofContext.set_defsort S)));
+
 
 (* notation *)
 
@@ -224,6 +232,9 @@
 val const_alias = alias Sign.const_alias ProofContext.const_alias;
 
 
+
+(** init and exit **)
+
 (* init *)
 
 fun init group theory_prefix operations target =

--- a/src/Pure/Isar/proof_context.ML	Wed Apr 28 11:13:11 2010 +0200
+++ b/src/Pure/Isar/proof_context.ML	Wed Apr 28 11:41:27 2010 +0200
@@ -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 set_defsort: sort -> Proof.context -> Proof.context
   val default_sort: Proof.context -> indexname -> sort
   val consts_of: Proof.context -> Consts.T
   val the_const_constraint: Proof.context -> string -> typ
@@ -178,12 +179,12 @@
 
 datatype ctxt =
   Ctxt of
-   {mode: mode,                       (*inner syntax mode*)
-    naming: Name_Space.naming,        (*local naming conventions*)
-    syntax: Local_Syntax.T,           (*local syntax*)
-    tsig: Type.tsig * Type.tsig,      (*local/global type signature -- local name space only*)
-    consts: Consts.T * Consts.T,      (*local/global consts -- local name space/abbrevs only*)
-    facts: Facts.T,                   (*local facts*)
+   {mode: mode,                  (*inner syntax mode*)
+    naming: Name_Space.naming,   (*local naming conventions*)
+    syntax: Local_Syntax.T,      (*local syntax*)
+    tsig: Type.tsig * Type.tsig, (*local/global type signature -- local name space / defsort only*)
+    consts: Consts.T * Consts.T, (*local/global consts -- local name space / abbrevs only*)
+    facts: Facts.T,              (*local facts*)
     cases: (string * (Rule_Cases.T * bool)) list};    (*named case contexts*)
 
 fun make_ctxt (mode, naming, syntax, tsig, consts, facts, cases) =
@@ -255,6 +256,7 @@
 val restore_syntax_mode = map_syntax o Local_Syntax.restore_mode o syntax_of;
 
 val tsig_of = #1 o #tsig o rep_context;
+val set_defsort = map_tsig o apfst o Type.set_defsort;
 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;