advanced translations: Context.generic;

--- a/doc-src/IsarRef/pure.tex	Mon Jan 30 15:31:31 2006 +0100
+++ b/doc-src/IsarRef/pure.tex	Tue Jan 31 00:39:40 2006 +0100
@@ -568,25 +568,26 @@
   (string * string * (string -> string * real)) list
 \end{ttbox}
 
-In case that the $(advanced)$ option is given, the corresponding translation
-functions may depend on the current theory context.  This allows to implement
-advanced syntax mechanisms, as translations functions may refer to specific
-theory declarations and auxiliary data.
+In case that the $(advanced)$ option is given, the corresponding
+translation functions may depend on the current theory or proof
+context.  This allows to implement advanced syntax mechanisms, as
+translations functions may refer to specific theory declarations or
+auxiliary proof data.
 
 See also \cite[\S8]{isabelle-ref} for more information on the general concept
 of syntax transformations in Isabelle.
 
 \begin{ttbox}
 val parse_ast_translation:
-  (string * (theory -> ast list -> ast)) list
+  (string * (Context.generic -> ast list -> ast)) list
 val parse_translation:
-  (string * (theory -> term list -> term)) list
+  (string * (Context.generic -> term list -> term)) list
 val print_translation:
-  (string * (theory -> term list -> term)) list
+  (string * (Context.generic -> term list -> term)) list
 val typed_print_translation:
-  (string * (theory -> bool -> typ -> term list -> term)) list
+  (string * (Context.generic -> bool -> typ -> term list -> term)) list
 val print_ast_translation:
-  (string * (theory -> ast list -> ast)) list
+  (string * (Context.generic -> ast list -> ast)) list
 \end{ttbox}
 
 

--- a/src/HOL/Tools/datatype_package.ML	Mon Jan 30 15:31:31 2006 +0100
+++ b/src/HOL/Tools/datatype_package.ML	Tue Jan 31 00:39:40 2006 +0100
@@ -442,19 +442,20 @@
 
 fun find_first f = Library.find_first f;
 
-fun case_tr sg [t, u] =
+fun case_tr context [t, u] =
     let
+      val thy = Context.theory_of context;
       fun case_error s name ts = raise TERM ("Error in case expression" ^
         getOpt (Option.map (curry op ^ " for datatype ") name, "") ^ ":\n" ^ s, ts);
       fun dest_case1 (Const ("_case1", _) $ t $ u) = (case strip_comb t of
-            (Const (s, _), ts) => (Sign.intern_const sg s, ts)
-          | (Free (s, _), ts) => (Sign.intern_const sg s, ts)
+            (Const (s, _), ts) => (Sign.intern_const thy s, ts)
+          | (Free (s, _), ts) => (Sign.intern_const thy s, ts)
           | _ => case_error "Head is not a constructor" NONE [t, u], u)
         | dest_case1 t = raise TERM ("dest_case1", [t]);
       fun dest_case2 (Const ("_case2", _) $ t $ u) = t :: dest_case2 u
         | dest_case2 t = [t];
       val cases as ((cname, _), _) :: _ = map dest_case1 (dest_case2 u);
-      val tab = Symtab.dest (get_datatypes sg);
+      val tab = Symtab.dest (get_datatypes thy);
       val (cases', default) = (case split_last cases of
           (cases', (("dummy_pattern", []), t)) => (cases', SOME t)
         | _ => (cases, NONE))
@@ -498,9 +499,9 @@
           | _ => list_comb (Syntax.const case_name, fs) $ t
         end
     end
-  | case_tr sg ts = raise TERM ("case_tr", ts);
+  | case_tr _ ts = raise TERM ("case_tr", ts);
 
-fun case_tr' constrs sg ts =
+fun case_tr' constrs context ts =
   if length ts <> length constrs + 1 then raise Match else
   let
     val (fs, x) = split_last ts;
@@ -516,7 +517,7 @@
         (loose_bnos (strip_abs_body t))
       end;
     val cases = map (fn ((cname, dts), t) =>
-      (Sign.extern_const sg cname,
+      (Sign.extern_const (Context.theory_of context) cname,
        strip_abs (length dts) t, is_dependent (length dts) t))
       (constrs ~~ fs);
     fun count_cases (cs, (_, _, true)) = cs

--- a/src/Pure/Isar/proof_context.ML	Mon Jan 30 15:31:31 2006 +0100
+++ b/src/Pure/Isar/proof_context.ML	Tue Jan 31 00:39:40 2006 +0100
@@ -355,7 +355,8 @@
 
 (** pretty printing **)
 
-fun pretty_term' thy ctxt t = Sign.pretty_term' (syn_of' thy ctxt) thy (context_tr' ctxt t);
+fun pretty_term' thy ctxt t =
+  Sign.pretty_term' (syn_of' thy ctxt) (Context.Proof ctxt) (context_tr' ctxt t);
 fun pretty_term ctxt t = pretty_term' (theory_of ctxt) ctxt (context_tr' ctxt t);
 fun pretty_typ ctxt T = Sign.pretty_typ (theory_of ctxt) T;
 fun pretty_sort ctxt S = Sign.pretty_sort (theory_of ctxt) S;
@@ -414,7 +415,7 @@
 local
 
 fun read_typ_aux read ctxt s =
-  read (syn_of ctxt) (theory_of ctxt, def_sort ctxt) s;
+  read (syn_of ctxt) (Context.Proof ctxt) (def_sort ctxt) s;
 
 fun cert_typ_aux cert ctxt raw_T =
   cert (theory_of ctxt) raw_T handle TYPE (msg, _, _) => error msg;
@@ -493,11 +494,12 @@
 
 (* read wrt. theory *)     (*exception ERROR*)
 
-fun read_def_termTs freeze pp syn thy (types, sorts, used) sTs =
-  Sign.read_def_terms' pp (Sign.is_logtype thy) syn (thy, types, sorts) used freeze sTs;
+fun read_def_termTs freeze pp syn ctxt (types, sorts, used) sTs =
+  Sign.read_def_terms' pp (Sign.is_logtype (theory_of ctxt)) syn
+    (Context.Proof ctxt) (types, sorts) used freeze sTs;
 
-fun read_def_termT freeze pp syn thy defaults sT =
-  apfst hd (read_def_termTs freeze pp syn thy defaults [sT]);
+fun read_def_termT freeze pp syn ctxt defaults sT =
+  apfst hd (read_def_termTs freeze pp syn ctxt defaults [sT]);
 
 fun read_term_thy freeze pp syn thy defaults s =
   #1 (read_def_termT freeze pp syn thy defaults (s, TypeInfer.logicT));
@@ -575,7 +577,7 @@
     val sorts = append_env (def_sort ctxt) more_sorts;
     val used = used_types ctxt @ more_used;
   in
-    (read (pp ctxt) (syn_of ctxt) (theory_of ctxt) (types, sorts, used) s
+    (read (pp ctxt) (syn_of ctxt) ctxt (types, sorts, used) s
       handle TERM (msg, _) => error msg)
     |> app (intern_skolem ctxt internal)
     |> app (if pattern then I else norm_term ctxt schematic)

--- a/src/Pure/Syntax/printer.ML	Mon Jan 30 15:31:31 2006 +0100
+++ b/src/Pure/Syntax/printer.ML	Tue Jan 31 00:39:40 2006 +0100
@@ -18,22 +18,22 @@
 signature PRINTER =
 sig
   include PRINTER0
-  val term_to_ast: theory -> (string -> (theory -> bool -> typ -> term list -> term) list) ->
-    term -> Ast.ast
-  val typ_to_ast: theory -> (string -> (theory -> bool -> typ -> term list -> term) list) ->
-    typ -> Ast.ast
-  val sort_to_ast: theory -> (string -> (theory -> bool -> typ -> term list -> term) list) ->
-    sort -> Ast.ast
+  val term_to_ast: Context.generic ->
+    (string -> (Context.generic -> bool -> typ -> term list -> term) list) -> term -> Ast.ast
+  val typ_to_ast: Context.generic ->
+    (string -> (Context.generic -> bool -> typ -> term list -> term) list) -> typ -> Ast.ast
+  val sort_to_ast: Context.generic ->
+    (string -> (Context.generic -> bool -> typ -> term list -> term) list) -> sort -> Ast.ast
   type prtabs
   val empty_prtabs: prtabs
   val extend_prtabs: string -> SynExt.xprod list -> prtabs -> prtabs
   val remove_prtabs: string -> SynExt.xprod list -> prtabs -> prtabs
   val merge_prtabs: prtabs -> prtabs -> prtabs
-  val pretty_term_ast: theory -> bool -> prtabs
-    -> (string -> (theory -> Ast.ast list -> Ast.ast) list)
+  val pretty_term_ast: Context.generic -> bool -> prtabs
+    -> (string -> (Context.generic -> Ast.ast list -> Ast.ast) list)
     -> (string -> (string -> string * real) option) -> Ast.ast -> Pretty.T
-  val pretty_typ_ast: theory -> bool -> prtabs
-    -> (string -> (theory -> Ast.ast list -> Ast.ast) list)
+  val pretty_typ_ast: Context.generic -> bool -> prtabs
+    -> (string -> (Context.generic -> Ast.ast list -> Ast.ast) list)
     -> (string -> (string -> string * real) option) -> Ast.ast -> Pretty.T
 end;
 
@@ -58,17 +58,17 @@
 
 (* apply print (ast) translation function *)
 
-fun apply_trans thy name a fns args =
+fun apply_trans context name a fns args =
   let
     fun app_first [] = raise Match
-      | app_first (f :: fs) = f thy args handle Match => app_first fs;
+      | app_first (f :: fs) = f context args handle Match => app_first fs;
   in
     transform_failure (fn Match => Match
       | exn => EXCEPTION (exn, "Error in " ^ name ^ " for " ^ quote a))
       app_first fns
   end;
 
-fun apply_typed x y fs = map (fn f => fn thy => f thy x y) fs;
+fun apply_typed x y fs = map (fn f => fn context => f context x y) fs;
 
 
 (* simple_ast_of *)
@@ -87,7 +87,7 @@
 
 (** sort_to_ast, typ_to_ast **)
 
-fun ast_of_termT thy trf tm =
+fun ast_of_termT context trf tm =
   let
     fun ast_of (t as Const ("_class", _) $ Free _) = simple_ast_of t
       | ast_of (t as Const ("_tfree", _) $ Free _) = simple_ast_of t
@@ -99,12 +99,12 @@
           | (f, args) => Ast.Appl (map ast_of (f :: args)))
       | ast_of t = simple_ast_of t
     and trans a args =
-      ast_of (apply_trans thy "print translation" a (apply_typed false dummyT (trf a)) args)
+      ast_of (apply_trans context "print translation" a (apply_typed false dummyT (trf a)) args)
         handle Match => Ast.mk_appl (Ast.Constant a) (map ast_of args);
   in ast_of tm end;
 
-fun sort_to_ast thy trf S = ast_of_termT thy trf (TypeExt.term_of_sort S);
-fun typ_to_ast thy trf T = ast_of_termT thy trf (TypeExt.term_of_typ (! show_sorts) T);
+fun sort_to_ast context trf S = ast_of_termT context trf (TypeExt.term_of_sort S);
+fun typ_to_ast context trf T = ast_of_termT context trf (TypeExt.term_of_typ (! show_sorts) T);
 
 
 
@@ -121,7 +121,7 @@
       else Lexicon.const "_var" $ t
   | mark_freevars a = a;
 
-fun ast_of_term thy trf show_all_types no_freeTs show_types show_sorts tm =
+fun ast_of_term context trf show_all_types no_freeTs show_types show_sorts tm =
   let
     fun prune_typs (t_seen as (Const _, _)) = t_seen
       | prune_typs (t as Free (x, ty), seen) =
@@ -158,13 +158,13 @@
       | (t, ts) => Ast.mk_appl (simple_ast_of t) (map ast_of ts))
 
     and trans a T args =
-      ast_of (apply_trans thy "print translation" a (apply_typed show_sorts T (trf a)) args)
+      ast_of (apply_trans context "print translation" a (apply_typed show_sorts T (trf a)) args)
         handle Match => Ast.mk_appl (Ast.Constant a) (map ast_of args)
 
     and constrain t T =
       if show_types andalso T <> dummyT then
         Ast.Appl [Ast.Constant SynExt.constrainC, simple_ast_of t,
-          ast_of_termT thy trf (TypeExt.term_of_typ show_sorts T)]
+          ast_of_termT context trf (TypeExt.term_of_typ show_sorts T)]
       else simple_ast_of t
   in
     tm
@@ -174,8 +174,8 @@
     |> ast_of
   end;
 
-fun term_to_ast thy trf tm =
-  ast_of_term thy trf (! show_all_types) (! show_no_free_types)
+fun term_to_ast context trf tm =
+  ast_of_term context trf (! show_all_types) (! show_no_free_types)
     (! show_types orelse ! show_sorts orelse ! show_all_types) (! show_sorts) tm;
 
 
@@ -265,9 +265,9 @@
   | is_chain [Arg _] = true
   | is_chain _  = false;
 
-fun pretty thy tabs trf tokentrf type_mode curried ast0 p0 =
+fun pretty context tabs trf tokentrf type_mode curried ast0 p0 =
   let
-    val trans = apply_trans thy "print ast translation";
+    val trans = apply_trans context "print ast translation";
 
     fun token_trans c [Ast.Variable x] =
           (case tokentrf c of
@@ -290,7 +290,7 @@
             val (Ts, args') = synT (symbs, args);
           in
             if type_mode then (astT (t, p) @ Ts, args')
-            else (pretty thy tabs trf tokentrf true curried t p @ Ts, args')
+            else (pretty context tabs trf tokentrf true curried t p @ Ts, args')
           end
       | synT (String s :: symbs, args) =
           let val (Ts, args') = synT (symbs, args);
@@ -353,15 +353,15 @@
 
 (* pretty_term_ast *)
 
-fun pretty_term_ast thy curried prtabs trf tokentrf ast =
-  Pretty.blk (0, pretty thy (mode_tabs prtabs (! print_mode))
+fun pretty_term_ast context curried prtabs trf tokentrf ast =
+  Pretty.blk (0, pretty context (mode_tabs prtabs (! print_mode))
     trf tokentrf false curried ast 0);
 
 
 (* pretty_typ_ast *)
 
-fun pretty_typ_ast thy _ prtabs trf tokentrf ast =
-  Pretty.blk (0, pretty thy (mode_tabs prtabs (! print_mode))
+fun pretty_typ_ast context _ prtabs trf tokentrf ast =
+  Pretty.blk (0, pretty context (mode_tabs prtabs (! print_mode))
     trf tokentrf true false ast 0);
 
 end;

--- a/src/Pure/Syntax/syn_ext.ML	Mon Jan 30 15:31:31 2006 +0100
+++ b/src/Pure/Syntax/syn_ext.ML	Tue Jan 31 00:39:40 2006 +0100
@@ -42,28 +42,32 @@
       xprods: xprod list,
       consts: string list,
       prmodes: string list,
-      parse_ast_translation: (string * ((theory -> Ast.ast list -> Ast.ast) * stamp)) list,
+      parse_ast_translation:
+        (string * ((Context.generic -> Ast.ast list -> Ast.ast) * stamp)) list,
       parse_rules: (Ast.ast * Ast.ast) list,
-      parse_translation: (string * ((theory -> term list -> term) * stamp)) list,
-      print_translation: (string * ((theory -> bool -> typ -> term list -> term) * stamp)) list,
+      parse_translation:
+        (string * ((Context.generic -> term list -> term) * stamp)) list,
+      print_translation:
+        (string * ((Context.generic -> bool -> typ -> term list -> term) * stamp)) list,
       print_rules: (Ast.ast * Ast.ast) list,
-      print_ast_translation: (string * ((theory -> Ast.ast list -> Ast.ast) * stamp)) list,
+      print_ast_translation:
+        (string * ((Context.generic -> Ast.ast list -> Ast.ast) * stamp)) list,
       token_translation: (string * string * (string -> string * real)) list}
   val mfix_args: string -> int
   val escape_mfix: string -> string
   val unlocalize_mfix: string -> string
   val syn_ext': bool -> (string -> bool) -> mfix list ->
-    string list -> (string * ((theory -> Ast.ast list -> Ast.ast) * stamp)) list *
-    (string * ((theory -> term list -> term) * stamp)) list *
-    (string * ((theory -> bool -> typ -> term list -> term) * stamp)) list *
-    (string * ((theory -> Ast.ast list -> Ast.ast) * stamp)) list
+    string list -> (string * ((Context.generic -> Ast.ast list -> Ast.ast) * stamp)) list *
+    (string * ((Context.generic -> term list -> term) * stamp)) list *
+    (string * ((Context.generic -> bool -> typ -> term list -> term) * stamp)) list *
+    (string * ((Context.generic -> Ast.ast list -> Ast.ast) * stamp)) list
     -> (string * string * (string -> string * real)) list
     -> (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext
   val syn_ext: mfix list -> string list ->
-    (string * ((theory -> Ast.ast list -> Ast.ast) * stamp)) list *
-    (string * ((theory -> term list -> term) * stamp)) list *
-    (string * ((theory -> bool -> typ -> term list -> term) * stamp)) list *
-    (string * ((theory -> Ast.ast list -> Ast.ast) * stamp)) list
+    (string * ((Context.generic -> Ast.ast list -> Ast.ast) * stamp)) list *
+    (string * ((Context.generic -> term list -> term) * stamp)) list *
+    (string * ((Context.generic -> bool -> typ -> term list -> term) * stamp)) list *
+    (string * ((Context.generic -> Ast.ast list -> Ast.ast) * stamp)) list
     -> (string * string * (string -> string * real)) list
     -> (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext
   val syn_ext_const_names: string list -> syn_ext
@@ -74,10 +78,10 @@
     (string * ((bool -> typ -> term list -> term) * stamp)) list *
     (string * ((Ast.ast list -> Ast.ast) * stamp)) list -> syn_ext
   val syn_ext_advanced_trfuns:
-    (string * ((theory -> Ast.ast list -> Ast.ast) * stamp)) list *
-    (string * ((theory -> term list -> term) * stamp)) list *
-    (string * ((theory -> bool -> typ -> term list -> term) * stamp)) list *
-    (string * ((theory -> Ast.ast list -> Ast.ast) * stamp)) list -> syn_ext
+    (string * ((Context.generic -> Ast.ast list -> Ast.ast) * stamp)) list *
+    (string * ((Context.generic -> term list -> term) * stamp)) list *
+    (string * ((Context.generic -> bool -> typ -> term list -> term) * stamp)) list *
+    (string * ((Context.generic -> Ast.ast list -> Ast.ast) * stamp)) list -> syn_ext
   val syn_ext_tokentrfuns: (string * string * (string -> string * real)) list -> syn_ext
   val standard_token_markers: string list
   val pure_ext: syn_ext
@@ -336,12 +340,16 @@
     xprods: xprod list,
     consts: string list,
     prmodes: string list,
-    parse_ast_translation: (string * ((theory -> Ast.ast list -> Ast.ast) * stamp)) list,
+    parse_ast_translation:
+      (string * ((Context.generic -> Ast.ast list -> Ast.ast) * stamp)) list,
     parse_rules: (Ast.ast * Ast.ast) list,
-    parse_translation: (string * ((theory -> term list -> term) * stamp)) list,
-    print_translation: (string * ((theory -> bool -> typ -> term list -> term) * stamp)) list,
+    parse_translation:
+      (string * ((Context.generic -> term list -> term) * stamp)) list,
+    print_translation:
+      (string * ((Context.generic -> bool -> typ -> term list -> term) * stamp)) list,
     print_rules: (Ast.ast * Ast.ast) list,
-    print_ast_translation: (string * ((theory -> Ast.ast list -> Ast.ast) * stamp)) list,
+    print_ast_translation:
+      (string * ((Context.generic -> Ast.ast list -> Ast.ast) * stamp)) list,
     token_translation: (string * string * (string -> string * real)) list};
 
 

--- a/src/Pure/Syntax/syn_trans.ML	Mon Jan 30 15:31:31 2006 +0100
+++ b/src/Pure/Syntax/syn_trans.ML	Tue Jan 31 00:39:40 2006 +0100
@@ -50,10 +50,11 @@
   val prop_tr': term -> term
   val appl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
   val applC_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
-  val pts_to_asts: theory -> (string -> (theory -> Ast.ast list -> Ast.ast) option) ->
+  val pts_to_asts: Context.generic ->
+    (string -> (Context.generic -> Ast.ast list -> Ast.ast) option) ->
     Parser.parsetree list -> Ast.ast list
-  val asts_to_terms: theory -> (string -> (theory -> term list -> term) option) ->
-    Ast.ast list -> term list
+  val asts_to_terms: Context.generic ->
+    (string -> (Context.generic -> term list -> term) option) -> Ast.ast list -> term list
 end;
 
 structure SynTrans: SYN_TRANS =
@@ -460,14 +461,14 @@
 
 (** pts_to_asts **)
 
-fun pts_to_asts thy trf pts =
+fun pts_to_asts context trf pts =
   let
     fun trans a args =
       (case trf a of
         NONE => Ast.mk_appl (Ast.Constant a) args
       | SOME f => transform_failure (fn exn =>
             EXCEPTION (exn, "Error in parse ast translation for " ^ quote a))
-          (fn () => f thy args) ());
+          (fn () => f context args) ());
 
     (*translate pt bottom-up*)
     fun ast_of (Parser.Node (a, pts)) = trans a (map ast_of pts)
@@ -484,14 +485,14 @@
 
 val fixedN = "\\<^fixed>";
 
-fun asts_to_terms thy trf asts =
+fun asts_to_terms context trf asts =
   let
     fun trans a args =
       (case trf a of
         NONE => Term.list_comb (Lexicon.const a, args)
       | SOME f => transform_failure (fn exn =>
             EXCEPTION (exn, "Error in parse translation for " ^ quote a))
-          (fn () => f thy args) ());
+          (fn () => f context args) ());
 
     fun term_of (Ast.Constant a) = trans a []
       | term_of (Ast.Variable x) = Lexicon.read_var x

--- a/src/Pure/Syntax/syntax.ML	Mon Jan 30 15:31:31 2006 +0100
+++ b/src/Pure/Syntax/syntax.ML	Tue Jan 31 00:39:40 2006 +0100
@@ -48,13 +48,13 @@
     (string * ((bool -> typ -> term list -> term) * stamp)) list *
     (string * ((ast list -> ast) * stamp)) list -> syntax -> syntax
   val extend_advanced_trfuns:
-    (string * ((theory -> ast list -> ast) * stamp)) list *
-    (string * ((theory -> term list -> term) * stamp)) list *
-    (string * ((theory -> bool -> typ -> term list -> term) * stamp)) list *
-    (string * ((theory -> ast list -> ast) * stamp)) list -> syntax -> syntax
+    (string * ((Context.generic -> ast list -> ast) * stamp)) list *
+    (string * ((Context.generic -> term list -> term) * stamp)) list *
+    (string * ((Context.generic -> bool -> typ -> term list -> term) * stamp)) list *
+    (string * ((Context.generic -> ast list -> ast) * stamp)) list -> syntax -> syntax
   val extend_tokentrfuns: (string * string * (string -> string * real)) list -> syntax -> syntax
   val extend_trrules_i: ast trrule list -> syntax -> syntax
-  val extend_trrules: theory -> (string -> bool) -> syntax ->
+  val extend_trrules: Context.generic -> (string -> bool) -> syntax ->
     (string * string) trrule list -> syntax -> syntax
   val remove_const_gram: (string -> bool) ->
     string * bool -> (string * typ * mixfix) list -> syntax -> syntax
@@ -67,13 +67,13 @@
   val print_gram: syntax -> unit
   val print_trans: syntax -> unit
   val print_syntax: syntax -> unit
-  val read: theory -> (string -> bool) -> syntax -> typ -> string -> term list
-  val read_typ: theory -> syntax -> ((indexname * sort) list -> indexname -> sort) ->
+  val read: Context.generic -> (string -> bool) -> syntax -> typ -> string -> term list
+  val read_typ: Context.generic -> syntax -> ((indexname * sort) list -> indexname -> sort) ->
     (sort -> sort) -> string -> typ
-  val read_sort: theory -> syntax -> string -> sort
-  val pretty_term: theory -> syntax -> bool -> term -> Pretty.T
-  val pretty_typ: theory -> syntax -> typ -> Pretty.T
-  val pretty_sort: theory -> syntax -> sort -> Pretty.T
+  val read_sort: Context.generic -> syntax -> string -> sort
+  val pretty_term: Context.generic -> syntax -> bool -> term -> Pretty.T
+  val pretty_typ: Context.generic -> syntax -> typ -> Pretty.T
+  val pretty_sort: Context.generic -> syntax -> sort -> Pretty.T
   val ambiguity_level: int ref
   val ambiguity_is_error: bool ref
 end;
@@ -169,12 +169,12 @@
     gram: Parser.gram,
     consts: string list,
     prmodes: string list,
-    parse_ast_trtab: ((theory -> Ast.ast list -> Ast.ast) * stamp) Symtab.table,
+    parse_ast_trtab: ((Context.generic -> Ast.ast list -> Ast.ast) * stamp) Symtab.table,
     parse_ruletab: ruletab,
-    parse_trtab: ((theory -> term list -> term) * stamp) Symtab.table,
-    print_trtab: ((theory -> bool -> typ -> term list -> term) * stamp) list Symtab.table,
+    parse_trtab: ((Context.generic -> term list -> term) * stamp) Symtab.table,
+    print_trtab: ((Context.generic -> bool -> typ -> term list -> term) * stamp) list Symtab.table,
     print_ruletab: ruletab,
-    print_ast_trtab: ((theory -> Ast.ast list -> Ast.ast) * stamp) list Symtab.table,
+    print_ast_trtab: ((Context.generic -> Ast.ast list -> Ast.ast) * stamp) list Symtab.table,
     tokentrtab: (string * (string * ((string -> string * real) * stamp)) list) list,
     prtabs: Printer.prtabs} * stamp;
 
@@ -376,7 +376,7 @@
 val ambiguity_level = ref 1;
 val ambiguity_is_error = ref false
 
-fun read_asts thy is_logtype (Syntax (tabs, _)) xids root str =
+fun read_asts context is_logtype (Syntax (tabs, _)) xids root str =
   let
     val {lexicon, gram, parse_ast_trtab, ...} = tabs;
     val root' = if root <> "prop" andalso is_logtype root then SynExt.logic else root;
@@ -384,41 +384,41 @@
     val pts = Parser.parse gram root' (Lexicon.tokenize lexicon xids chars);
 
     fun show_pt pt =
-      Pretty.string_of (Ast.pretty_ast (hd (SynTrans.pts_to_asts thy (K NONE) [pt])));
+      Pretty.string_of (Ast.pretty_ast (hd (SynTrans.pts_to_asts context (K NONE) [pt])));
   in
     conditional (length pts > ! ambiguity_level) (fn () =>
       if ! ambiguity_is_error then error ("Ambiguous input " ^ quote str)
       else (warning ("Ambiguous input " ^ quote str ^ "\n" ^
           "produces " ^ string_of_int (length pts) ^ " parse trees.");
          List.app (warning o show_pt) pts));
-    SynTrans.pts_to_asts thy (lookup_tr parse_ast_trtab) pts
+    SynTrans.pts_to_asts context (lookup_tr parse_ast_trtab) pts
   end;
 
 
 (* read *)
 
-fun read thy is_logtype (syn as Syntax (tabs, _)) ty str =
+fun read context is_logtype (syn as Syntax (tabs, _)) ty str =
   let
     val {parse_ruletab, parse_trtab, ...} = tabs;
-    val asts = read_asts thy is_logtype syn false (SynExt.typ_to_nonterm ty) str;
+    val asts = read_asts context is_logtype syn false (SynExt.typ_to_nonterm ty) str;
   in
-    SynTrans.asts_to_terms thy (lookup_tr parse_trtab)
+    SynTrans.asts_to_terms context (lookup_tr parse_trtab)
       (map (Ast.normalize_ast (Symtab.lookup_multi parse_ruletab)) asts)
   end;
 
 
 (* read types *)
 
-fun read_typ thy syn get_sort map_sort str =
-  (case read thy (K false) syn SynExt.typeT str of
+fun read_typ context syn get_sort map_sort str =
+  (case read context (K false) syn SynExt.typeT str of
     [t] => TypeExt.typ_of_term (get_sort (TypeExt.raw_term_sorts t)) map_sort t
   | _ => error "read_typ: ambiguous syntax");
 
 
 (* read sorts *)
 
-fun read_sort thy syn str =
-  (case read thy (K false) syn TypeExt.sortT str of
+fun read_sort context syn str =
+  (case read context (K false) syn TypeExt.sortT str of
     [t] => TypeExt.sort_of_term t
   | _ => error "read_sort: ambiguous syntax");
 
@@ -452,7 +452,7 @@
   | NONE => rule);
 
 
-fun read_pattern thy is_logtype syn (root, str) =
+fun read_pattern context is_logtype syn (root, str) =
   let
     val Syntax ({consts, ...}, _) = syn;
 
@@ -462,7 +462,7 @@
           else ast
       | constify (Ast.Appl asts) = Ast.Appl (map constify asts);
   in
-    (case read_asts thy is_logtype syn true root str of
+    (case read_asts context is_logtype syn true root str of
       [ast] => constify ast
     | _ => error ("Syntactically ambiguous input: " ^ quote str))
   end handle ERROR msg =>
@@ -480,19 +480,19 @@
 
 (** pretty terms, typs, sorts **)
 
-fun pretty_t t_to_ast prt_t thy (syn as Syntax (tabs, _)) curried t =
+fun pretty_t t_to_ast prt_t context (syn as Syntax (tabs, _)) curried t =
   let
     val {print_trtab, print_ruletab, print_ast_trtab, tokentrtab, prtabs, ...} = tabs;
-    val ast = t_to_ast thy (lookup_tr' print_trtab) t;
+    val ast = t_to_ast context (lookup_tr' print_trtab) t;
   in
-    prt_t thy curried prtabs (lookup_tr' print_ast_trtab)
+    prt_t context curried prtabs (lookup_tr' print_ast_trtab)
       (lookup_tokentr tokentrtab (! print_mode))
       (Ast.normalize_ast (Symtab.lookup_multi print_ruletab) ast)
   end;
 
 val pretty_term = pretty_t Printer.term_to_ast Printer.pretty_term_ast;
-fun pretty_typ thy syn = pretty_t Printer.typ_to_ast Printer.pretty_typ_ast thy syn false;
-fun pretty_sort thy syn = pretty_t Printer.sort_to_ast Printer.pretty_typ_ast thy syn false;
+fun pretty_typ context syn = pretty_t Printer.typ_to_ast Printer.pretty_typ_ast context syn false;
+fun pretty_sort context syn = pretty_t Printer.sort_to_ast Printer.pretty_typ_ast context syn false;
 
 
 
@@ -509,9 +509,9 @@
 val extend_tokentrfuns     = ext_syntax SynExt.syn_ext_tokentrfuns;
 val extend_trrules_i       = ext_syntax SynExt.syn_ext_rules o prep_rules I;
 
-fun extend_trrules thy is_logtype syn rules =
+fun extend_trrules context is_logtype syn rules =
   ext_syntax' (K SynExt.syn_ext_rules) (K false) default_mode
-    (prep_rules (read_pattern thy is_logtype syn) rules);
+    (prep_rules (read_pattern context is_logtype syn) rules);
 
 fun remove_const_gram is_logtype prmode decls =
   remove_syntax prmode (Mixfix.syn_ext_consts is_logtype decls);

--- a/src/Pure/sign.ML	Mon Jan 30 15:31:31 2006 +0100
+++ b/src/Pure/sign.ML	Tue Jan 31 00:39:40 2006 +0100
@@ -39,12 +39,12 @@
   val add_trfunsT:
     (string * (bool -> typ -> term list -> term)) list -> theory -> theory
   val add_advanced_trfuns:
-    (string * (theory -> ast list -> ast)) list *
-    (string * (theory -> term list -> term)) list *
-    (string * (theory -> term list -> term)) list *
-    (string * (theory -> ast list -> ast)) list -> theory -> theory
+    (string * (Context.generic -> ast list -> ast)) list *
+    (string * (Context.generic -> term list -> term)) list *
+    (string * (Context.generic -> term list -> term)) list *
+    (string * (Context.generic -> ast list -> ast)) list -> theory -> theory
   val add_advanced_trfunsT:
-    (string * (theory -> bool -> typ -> term list -> term)) list -> theory -> theory
+    (string * (Context.generic -> bool -> typ -> term list -> term)) list -> theory -> theory
   val add_tokentrfuns:
     (string * string * (string -> string * real)) list -> theory -> theory
   val add_mode_tokentrfuns: string -> (string * (string -> string * real)) list
@@ -132,7 +132,7 @@
   val intern_term: theory -> term -> term
   val extern_term: theory -> term -> term
   val intern_tycons: theory -> typ -> typ
-  val pretty_term': Syntax.syntax -> theory -> term -> Pretty.T
+  val pretty_term': Syntax.syntax -> Context.generic -> term -> Pretty.T
   val pretty_term: theory -> term -> Pretty.T
   val pretty_typ: theory -> typ -> Pretty.T
   val pretty_sort: theory -> sort -> Pretty.T
@@ -155,11 +155,14 @@
   val certify_prop: Pretty.pp -> theory -> term -> term * typ * int
   val cert_term: theory -> term -> term
   val cert_prop: theory -> term -> term
-  val read_sort': Syntax.syntax -> theory -> string -> sort
+  val read_sort': Syntax.syntax -> Context.generic -> string -> sort
   val read_sort: theory -> string -> sort
-  val read_typ': Syntax.syntax -> theory * (indexname -> sort option) -> string -> typ
-  val read_typ_syntax': Syntax.syntax -> theory * (indexname -> sort option) -> string -> typ
-  val read_typ_abbrev': Syntax.syntax -> theory * (indexname -> sort option) -> string -> typ
+  val read_typ': Syntax.syntax -> Context.generic ->
+    (indexname -> sort option) -> string -> typ
+  val read_typ_syntax': Syntax.syntax -> Context.generic ->
+    (indexname -> sort option) -> string -> typ
+  val read_typ_abbrev': Syntax.syntax -> Context.generic ->
+    (indexname -> sort option) -> string -> typ
   val read_typ: theory * (indexname -> sort option) -> string -> typ
   val read_typ_syntax: theory * (indexname -> sort option) -> string -> typ
   val read_typ_abbrev: theory * (indexname -> sort option) -> string -> typ
@@ -171,8 +174,8 @@
   val infer_types: Pretty.pp -> theory -> (indexname -> typ option) ->
     (indexname -> sort option) -> string list -> bool
     -> term list * typ -> term * (indexname * typ) list
-  val read_def_terms': Pretty.pp -> (string -> bool) -> Syntax.syntax ->
-    theory * (indexname -> typ option) * (indexname -> sort option) ->
+  val read_def_terms': Pretty.pp -> (string -> bool) -> Syntax.syntax -> Context.generic ->
+    (indexname -> typ option) * (indexname -> sort option) ->
     string list -> bool -> (string * typ) list -> term list * (indexname * typ) list
   val read_def_terms:
     theory * (indexname -> typ option) * (indexname -> sort option) ->
@@ -338,11 +341,16 @@
 
 (** pretty printing of terms, types etc. **)
 
-fun pretty_term' syn thy t =
-  Syntax.pretty_term thy syn (Context.exists_name Context.CPureN thy) (extern_term thy t);
-fun pretty_term thy t = pretty_term' (syn_of thy) thy t;
-fun pretty_typ thy T = Syntax.pretty_typ thy (syn_of thy) (extern_typ thy T);
-fun pretty_sort thy S = Syntax.pretty_sort thy (syn_of thy) (extern_sort thy S);
+fun pretty_term' syn context t =
+  let
+    val thy = Context.theory_of context;
+    val curried = Context.exists_name Context.CPureN thy;
+  in Syntax.pretty_term context syn curried (extern_term thy t) end;
+
+fun pretty_term thy t = pretty_term' (syn_of thy) (Context.Theory thy) t;
+
+fun pretty_typ thy T = Syntax.pretty_typ (Context.Theory thy) (syn_of thy) (extern_typ thy T);
+fun pretty_sort thy S = Syntax.pretty_sort (Context.Theory thy) (syn_of thy) (extern_sort thy S);
 
 fun pretty_classrel thy cs = Pretty.block (List.concat
   (separate [Pretty.str " <", Pretty.brk 1] (map (single o pretty_sort thy o single) cs)));
@@ -458,29 +466,31 @@
 
 (* sorts *)
 
-fun read_sort' syn thy str =
+fun read_sort' syn context str =
   let
+    val thy = Context.theory_of context;
     val _ = Context.check_thy thy;
-    val S = intern_sort thy (Syntax.read_sort thy syn str);
+    val S = intern_sort thy (Syntax.read_sort context syn str);
   in certify_sort thy S handle TYPE (msg, _, _) => error msg end;
 
-fun read_sort thy str = read_sort' (syn_of thy) thy str;
+fun read_sort thy str = read_sort' (syn_of thy) (Context.Theory thy) str;
 
 
 (* types *)
 
 local
 
-fun gen_read_typ' cert syn (thy, def_sort) str =
+fun gen_read_typ' cert syn context def_sort str =
   let
+    val thy = Context.theory_of context;
     val _ = Context.check_thy thy;
     val get_sort = TypeInfer.get_sort (tsig_of thy) def_sort (intern_sort thy);
-    val T = intern_tycons thy (Syntax.read_typ thy syn get_sort (intern_sort thy) str);
+    val T = intern_tycons thy (Syntax.read_typ context syn get_sort (intern_sort thy) str);
   in cert thy T handle TYPE (msg, _, _) => error msg end
   handle ERROR msg => cat_error msg ("The error(s) above occurred in type " ^ quote str);
 
 fun gen_read_typ cert (thy, def_sort) str =
-  gen_read_typ' cert (syn_of thy) (thy, def_sort) str;
+  gen_read_typ' cert (syn_of thy) (Context.Theory thy) def_sort str;
 
 in
 
@@ -563,15 +573,16 @@
 
 (* read_def_terms -- read terms and infer types *)    (*exception ERROR*)
 
-fun read_def_terms' pp is_logtype syn (thy, types, sorts) used freeze sTs =
+fun read_def_terms' pp is_logtype syn context (types, sorts) used freeze sTs =
   let
+    val thy = Context.theory_of context;
     fun read (s, T) =
       let val T' = certify_typ thy T handle TYPE (msg, _, _) => error msg
-      in (Syntax.read thy is_logtype syn T' s, T') end;
+      in (Syntax.read context is_logtype syn T' s, T') end;
   in infer_types_simult pp thy types sorts used freeze (map read sTs) end;
 
 fun read_def_terms (thy, types, sorts) =
-  read_def_terms' (pp thy) (is_logtype thy) (syn_of thy) (thy, types, sorts);
+  read_def_terms' (pp thy) (is_logtype thy) (syn_of thy) (Context.Theory thy) (types, sorts);
 
 fun simple_read_term thy T s =
   let val ([t], _) = read_def_terms (thy, K NONE, K NONE) [] true [(s, T)]
@@ -770,7 +781,7 @@
 local
 
 fun advancedT false = ""
-  | advancedT true = "theory -> ";
+  | advancedT true = "Context.generic -> ";
 
 fun advancedN false = ""
   | advancedN true = "advanced_";
@@ -813,7 +824,7 @@
 
 fun add_trrules args thy = thy |> map_syn (fn syn =>
   let val rules = map (Syntax.map_trrule (apfst (intern_type thy))) args
-  in Syntax.extend_trrules thy (is_logtype thy) syn rules syn end);
+  in Syntax.extend_trrules (Context.Theory thy) (is_logtype thy) syn rules syn end);
 
 val add_trrules_i = map_syn o Syntax.extend_trrules_i;
 

--- a/src/Pure/theory.ML	Mon Jan 30 15:31:31 2006 +0100
+++ b/src/Pure/theory.ML	Tue Jan 31 00:39:40 2006 +0100
@@ -187,7 +187,7 @@
 
 fun read_def_axm (thy, types, sorts) used (name, str) =
   let
-    val ts = Syntax.read thy (Sign.is_logtype thy) (Sign.syn_of thy) propT str;
+    val ts = Syntax.read (Context.Theory thy) (Sign.is_logtype thy) (Sign.syn_of thy) propT str;
     val (t, _) = Sign.infer_types (Sign.pp thy) thy types sorts used true (ts, propT);
   in cert_axm thy (name, t) end
   handle ERROR msg => err_in_axm msg name;