advanced translations: Context.generic;
authorwenzelm
Tue Jan 31 00:39:40 2006 +0100 (2006-01-31)
changeset 18857c4b4fbd74ffb
parent 18856 4669dec681f4
child 18858 ceb93f3af7f0
advanced translations: Context.generic;
doc-src/IsarRef/pure.tex
src/HOL/Tools/datatype_package.ML
src/Pure/Isar/proof_context.ML
src/Pure/Syntax/printer.ML
src/Pure/Syntax/syn_ext.ML
src/Pure/Syntax/syn_trans.ML
src/Pure/Syntax/syntax.ML
src/Pure/sign.ML
src/Pure/theory.ML
     1.1 --- a/doc-src/IsarRef/pure.tex	Mon Jan 30 15:31:31 2006 +0100
     1.2 +++ b/doc-src/IsarRef/pure.tex	Tue Jan 31 00:39:40 2006 +0100
     1.3 @@ -568,25 +568,26 @@
     1.4    (string * string * (string -> string * real)) list
     1.5  \end{ttbox}
     1.6  
     1.7 -In case that the $(advanced)$ option is given, the corresponding translation
     1.8 -functions may depend on the current theory context.  This allows to implement
     1.9 -advanced syntax mechanisms, as translations functions may refer to specific
    1.10 -theory declarations and auxiliary data.
    1.11 +In case that the $(advanced)$ option is given, the corresponding
    1.12 +translation functions may depend on the current theory or proof
    1.13 +context.  This allows to implement advanced syntax mechanisms, as
    1.14 +translations functions may refer to specific theory declarations or
    1.15 +auxiliary proof data.
    1.16  
    1.17  See also \cite[\S8]{isabelle-ref} for more information on the general concept
    1.18  of syntax transformations in Isabelle.
    1.19  
    1.20  \begin{ttbox}
    1.21  val parse_ast_translation:
    1.22 -  (string * (theory -> ast list -> ast)) list
    1.23 +  (string * (Context.generic -> ast list -> ast)) list
    1.24  val parse_translation:
    1.25 -  (string * (theory -> term list -> term)) list
    1.26 +  (string * (Context.generic -> term list -> term)) list
    1.27  val print_translation:
    1.28 -  (string * (theory -> term list -> term)) list
    1.29 +  (string * (Context.generic -> term list -> term)) list
    1.30  val typed_print_translation:
    1.31 -  (string * (theory -> bool -> typ -> term list -> term)) list
    1.32 +  (string * (Context.generic -> bool -> typ -> term list -> term)) list
    1.33  val print_ast_translation:
    1.34 -  (string * (theory -> ast list -> ast)) list
    1.35 +  (string * (Context.generic -> ast list -> ast)) list
    1.36  \end{ttbox}
    1.37  
    1.38  
     2.1 --- a/src/HOL/Tools/datatype_package.ML	Mon Jan 30 15:31:31 2006 +0100
     2.2 +++ b/src/HOL/Tools/datatype_package.ML	Tue Jan 31 00:39:40 2006 +0100
     2.3 @@ -442,19 +442,20 @@
     2.4  
     2.5  fun find_first f = Library.find_first f;
     2.6  
     2.7 -fun case_tr sg [t, u] =
     2.8 +fun case_tr context [t, u] =
     2.9      let
    2.10 +      val thy = Context.theory_of context;
    2.11        fun case_error s name ts = raise TERM ("Error in case expression" ^
    2.12          getOpt (Option.map (curry op ^ " for datatype ") name, "") ^ ":\n" ^ s, ts);
    2.13        fun dest_case1 (Const ("_case1", _) $ t $ u) = (case strip_comb t of
    2.14 -            (Const (s, _), ts) => (Sign.intern_const sg s, ts)
    2.15 -          | (Free (s, _), ts) => (Sign.intern_const sg s, ts)
    2.16 +            (Const (s, _), ts) => (Sign.intern_const thy s, ts)
    2.17 +          | (Free (s, _), ts) => (Sign.intern_const thy s, ts)
    2.18            | _ => case_error "Head is not a constructor" NONE [t, u], u)
    2.19          | dest_case1 t = raise TERM ("dest_case1", [t]);
    2.20        fun dest_case2 (Const ("_case2", _) $ t $ u) = t :: dest_case2 u
    2.21          | dest_case2 t = [t];
    2.22        val cases as ((cname, _), _) :: _ = map dest_case1 (dest_case2 u);
    2.23 -      val tab = Symtab.dest (get_datatypes sg);
    2.24 +      val tab = Symtab.dest (get_datatypes thy);
    2.25        val (cases', default) = (case split_last cases of
    2.26            (cases', (("dummy_pattern", []), t)) => (cases', SOME t)
    2.27          | _ => (cases, NONE))
    2.28 @@ -498,9 +499,9 @@
    2.29            | _ => list_comb (Syntax.const case_name, fs) $ t
    2.30          end
    2.31      end
    2.32 -  | case_tr sg ts = raise TERM ("case_tr", ts);
    2.33 +  | case_tr _ ts = raise TERM ("case_tr", ts);
    2.34  
    2.35 -fun case_tr' constrs sg ts =
    2.36 +fun case_tr' constrs context ts =
    2.37    if length ts <> length constrs + 1 then raise Match else
    2.38    let
    2.39      val (fs, x) = split_last ts;
    2.40 @@ -516,7 +517,7 @@
    2.41          (loose_bnos (strip_abs_body t))
    2.42        end;
    2.43      val cases = map (fn ((cname, dts), t) =>
    2.44 -      (Sign.extern_const sg cname,
    2.45 +      (Sign.extern_const (Context.theory_of context) cname,
    2.46         strip_abs (length dts) t, is_dependent (length dts) t))
    2.47        (constrs ~~ fs);
    2.48      fun count_cases (cs, (_, _, true)) = cs
     3.1 --- a/src/Pure/Isar/proof_context.ML	Mon Jan 30 15:31:31 2006 +0100
     3.2 +++ b/src/Pure/Isar/proof_context.ML	Tue Jan 31 00:39:40 2006 +0100
     3.3 @@ -355,7 +355,8 @@
     3.4  
     3.5  (** pretty printing **)
     3.6  
     3.7 -fun pretty_term' thy ctxt t = Sign.pretty_term' (syn_of' thy ctxt) thy (context_tr' ctxt t);
     3.8 +fun pretty_term' thy ctxt t =
     3.9 +  Sign.pretty_term' (syn_of' thy ctxt) (Context.Proof ctxt) (context_tr' ctxt t);
    3.10  fun pretty_term ctxt t = pretty_term' (theory_of ctxt) ctxt (context_tr' ctxt t);
    3.11  fun pretty_typ ctxt T = Sign.pretty_typ (theory_of ctxt) T;
    3.12  fun pretty_sort ctxt S = Sign.pretty_sort (theory_of ctxt) S;
    3.13 @@ -414,7 +415,7 @@
    3.14  local
    3.15  
    3.16  fun read_typ_aux read ctxt s =
    3.17 -  read (syn_of ctxt) (theory_of ctxt, def_sort ctxt) s;
    3.18 +  read (syn_of ctxt) (Context.Proof ctxt) (def_sort ctxt) s;
    3.19  
    3.20  fun cert_typ_aux cert ctxt raw_T =
    3.21    cert (theory_of ctxt) raw_T handle TYPE (msg, _, _) => error msg;
    3.22 @@ -493,11 +494,12 @@
    3.23  
    3.24  (* read wrt. theory *)     (*exception ERROR*)
    3.25  
    3.26 -fun read_def_termTs freeze pp syn thy (types, sorts, used) sTs =
    3.27 -  Sign.read_def_terms' pp (Sign.is_logtype thy) syn (thy, types, sorts) used freeze sTs;
    3.28 +fun read_def_termTs freeze pp syn ctxt (types, sorts, used) sTs =
    3.29 +  Sign.read_def_terms' pp (Sign.is_logtype (theory_of ctxt)) syn
    3.30 +    (Context.Proof ctxt) (types, sorts) used freeze sTs;
    3.31  
    3.32 -fun read_def_termT freeze pp syn thy defaults sT =
    3.33 -  apfst hd (read_def_termTs freeze pp syn thy defaults [sT]);
    3.34 +fun read_def_termT freeze pp syn ctxt defaults sT =
    3.35 +  apfst hd (read_def_termTs freeze pp syn ctxt defaults [sT]);
    3.36  
    3.37  fun read_term_thy freeze pp syn thy defaults s =
    3.38    #1 (read_def_termT freeze pp syn thy defaults (s, TypeInfer.logicT));
    3.39 @@ -575,7 +577,7 @@
    3.40      val sorts = append_env (def_sort ctxt) more_sorts;
    3.41      val used = used_types ctxt @ more_used;
    3.42    in
    3.43 -    (read (pp ctxt) (syn_of ctxt) (theory_of ctxt) (types, sorts, used) s
    3.44 +    (read (pp ctxt) (syn_of ctxt) ctxt (types, sorts, used) s
    3.45        handle TERM (msg, _) => error msg)
    3.46      |> app (intern_skolem ctxt internal)
    3.47      |> app (if pattern then I else norm_term ctxt schematic)
     4.1 --- a/src/Pure/Syntax/printer.ML	Mon Jan 30 15:31:31 2006 +0100
     4.2 +++ b/src/Pure/Syntax/printer.ML	Tue Jan 31 00:39:40 2006 +0100
     4.3 @@ -18,22 +18,22 @@
     4.4  signature PRINTER =
     4.5  sig
     4.6    include PRINTER0
     4.7 -  val term_to_ast: theory -> (string -> (theory -> bool -> typ -> term list -> term) list) ->
     4.8 -    term -> Ast.ast
     4.9 -  val typ_to_ast: theory -> (string -> (theory -> bool -> typ -> term list -> term) list) ->
    4.10 -    typ -> Ast.ast
    4.11 -  val sort_to_ast: theory -> (string -> (theory -> bool -> typ -> term list -> term) list) ->
    4.12 -    sort -> Ast.ast
    4.13 +  val term_to_ast: Context.generic ->
    4.14 +    (string -> (Context.generic -> bool -> typ -> term list -> term) list) -> term -> Ast.ast
    4.15 +  val typ_to_ast: Context.generic ->
    4.16 +    (string -> (Context.generic -> bool -> typ -> term list -> term) list) -> typ -> Ast.ast
    4.17 +  val sort_to_ast: Context.generic ->
    4.18 +    (string -> (Context.generic -> bool -> typ -> term list -> term) list) -> sort -> Ast.ast
    4.19    type prtabs
    4.20    val empty_prtabs: prtabs
    4.21    val extend_prtabs: string -> SynExt.xprod list -> prtabs -> prtabs
    4.22    val remove_prtabs: string -> SynExt.xprod list -> prtabs -> prtabs
    4.23    val merge_prtabs: prtabs -> prtabs -> prtabs
    4.24 -  val pretty_term_ast: theory -> bool -> prtabs
    4.25 -    -> (string -> (theory -> Ast.ast list -> Ast.ast) list)
    4.26 +  val pretty_term_ast: Context.generic -> bool -> prtabs
    4.27 +    -> (string -> (Context.generic -> Ast.ast list -> Ast.ast) list)
    4.28      -> (string -> (string -> string * real) option) -> Ast.ast -> Pretty.T
    4.29 -  val pretty_typ_ast: theory -> bool -> prtabs
    4.30 -    -> (string -> (theory -> Ast.ast list -> Ast.ast) list)
    4.31 +  val pretty_typ_ast: Context.generic -> bool -> prtabs
    4.32 +    -> (string -> (Context.generic -> Ast.ast list -> Ast.ast) list)
    4.33      -> (string -> (string -> string * real) option) -> Ast.ast -> Pretty.T
    4.34  end;
    4.35  
    4.36 @@ -58,17 +58,17 @@
    4.37  
    4.38  (* apply print (ast) translation function *)
    4.39  
    4.40 -fun apply_trans thy name a fns args =
    4.41 +fun apply_trans context name a fns args =
    4.42    let
    4.43      fun app_first [] = raise Match
    4.44 -      | app_first (f :: fs) = f thy args handle Match => app_first fs;
    4.45 +      | app_first (f :: fs) = f context args handle Match => app_first fs;
    4.46    in
    4.47      transform_failure (fn Match => Match
    4.48        | exn => EXCEPTION (exn, "Error in " ^ name ^ " for " ^ quote a))
    4.49        app_first fns
    4.50    end;
    4.51  
    4.52 -fun apply_typed x y fs = map (fn f => fn thy => f thy x y) fs;
    4.53 +fun apply_typed x y fs = map (fn f => fn context => f context x y) fs;
    4.54  
    4.55  
    4.56  (* simple_ast_of *)
    4.57 @@ -87,7 +87,7 @@
    4.58  
    4.59  (** sort_to_ast, typ_to_ast **)
    4.60  
    4.61 -fun ast_of_termT thy trf tm =
    4.62 +fun ast_of_termT context trf tm =
    4.63    let
    4.64      fun ast_of (t as Const ("_class", _) $ Free _) = simple_ast_of t
    4.65        | ast_of (t as Const ("_tfree", _) $ Free _) = simple_ast_of t
    4.66 @@ -99,12 +99,12 @@
    4.67            | (f, args) => Ast.Appl (map ast_of (f :: args)))
    4.68        | ast_of t = simple_ast_of t
    4.69      and trans a args =
    4.70 -      ast_of (apply_trans thy "print translation" a (apply_typed false dummyT (trf a)) args)
    4.71 +      ast_of (apply_trans context "print translation" a (apply_typed false dummyT (trf a)) args)
    4.72          handle Match => Ast.mk_appl (Ast.Constant a) (map ast_of args);
    4.73    in ast_of tm end;
    4.74  
    4.75 -fun sort_to_ast thy trf S = ast_of_termT thy trf (TypeExt.term_of_sort S);
    4.76 -fun typ_to_ast thy trf T = ast_of_termT thy trf (TypeExt.term_of_typ (! show_sorts) T);
    4.77 +fun sort_to_ast context trf S = ast_of_termT context trf (TypeExt.term_of_sort S);
    4.78 +fun typ_to_ast context trf T = ast_of_termT context trf (TypeExt.term_of_typ (! show_sorts) T);
    4.79  
    4.80  
    4.81  
    4.82 @@ -121,7 +121,7 @@
    4.83        else Lexicon.const "_var" $ t
    4.84    | mark_freevars a = a;
    4.85  
    4.86 -fun ast_of_term thy trf show_all_types no_freeTs show_types show_sorts tm =
    4.87 +fun ast_of_term context trf show_all_types no_freeTs show_types show_sorts tm =
    4.88    let
    4.89      fun prune_typs (t_seen as (Const _, _)) = t_seen
    4.90        | prune_typs (t as Free (x, ty), seen) =
    4.91 @@ -158,13 +158,13 @@
    4.92        | (t, ts) => Ast.mk_appl (simple_ast_of t) (map ast_of ts))
    4.93  
    4.94      and trans a T args =
    4.95 -      ast_of (apply_trans thy "print translation" a (apply_typed show_sorts T (trf a)) args)
    4.96 +      ast_of (apply_trans context "print translation" a (apply_typed show_sorts T (trf a)) args)
    4.97          handle Match => Ast.mk_appl (Ast.Constant a) (map ast_of args)
    4.98  
    4.99      and constrain t T =
   4.100        if show_types andalso T <> dummyT then
   4.101          Ast.Appl [Ast.Constant SynExt.constrainC, simple_ast_of t,
   4.102 -          ast_of_termT thy trf (TypeExt.term_of_typ show_sorts T)]
   4.103 +          ast_of_termT context trf (TypeExt.term_of_typ show_sorts T)]
   4.104        else simple_ast_of t
   4.105    in
   4.106      tm
   4.107 @@ -174,8 +174,8 @@
   4.108      |> ast_of
   4.109    end;
   4.110  
   4.111 -fun term_to_ast thy trf tm =
   4.112 -  ast_of_term thy trf (! show_all_types) (! show_no_free_types)
   4.113 +fun term_to_ast context trf tm =
   4.114 +  ast_of_term context trf (! show_all_types) (! show_no_free_types)
   4.115      (! show_types orelse ! show_sorts orelse ! show_all_types) (! show_sorts) tm;
   4.116  
   4.117  
   4.118 @@ -265,9 +265,9 @@
   4.119    | is_chain [Arg _] = true
   4.120    | is_chain _  = false;
   4.121  
   4.122 -fun pretty thy tabs trf tokentrf type_mode curried ast0 p0 =
   4.123 +fun pretty context tabs trf tokentrf type_mode curried ast0 p0 =
   4.124    let
   4.125 -    val trans = apply_trans thy "print ast translation";
   4.126 +    val trans = apply_trans context "print ast translation";
   4.127  
   4.128      fun token_trans c [Ast.Variable x] =
   4.129            (case tokentrf c of
   4.130 @@ -290,7 +290,7 @@
   4.131              val (Ts, args') = synT (symbs, args);
   4.132            in
   4.133              if type_mode then (astT (t, p) @ Ts, args')
   4.134 -            else (pretty thy tabs trf tokentrf true curried t p @ Ts, args')
   4.135 +            else (pretty context tabs trf tokentrf true curried t p @ Ts, args')
   4.136            end
   4.137        | synT (String s :: symbs, args) =
   4.138            let val (Ts, args') = synT (symbs, args);
   4.139 @@ -353,15 +353,15 @@
   4.140  
   4.141  (* pretty_term_ast *)
   4.142  
   4.143 -fun pretty_term_ast thy curried prtabs trf tokentrf ast =
   4.144 -  Pretty.blk (0, pretty thy (mode_tabs prtabs (! print_mode))
   4.145 +fun pretty_term_ast context curried prtabs trf tokentrf ast =
   4.146 +  Pretty.blk (0, pretty context (mode_tabs prtabs (! print_mode))
   4.147      trf tokentrf false curried ast 0);
   4.148  
   4.149  
   4.150  (* pretty_typ_ast *)
   4.151  
   4.152 -fun pretty_typ_ast thy _ prtabs trf tokentrf ast =
   4.153 -  Pretty.blk (0, pretty thy (mode_tabs prtabs (! print_mode))
   4.154 +fun pretty_typ_ast context _ prtabs trf tokentrf ast =
   4.155 +  Pretty.blk (0, pretty context (mode_tabs prtabs (! print_mode))
   4.156      trf tokentrf true false ast 0);
   4.157  
   4.158  end;
     5.1 --- a/src/Pure/Syntax/syn_ext.ML	Mon Jan 30 15:31:31 2006 +0100
     5.2 +++ b/src/Pure/Syntax/syn_ext.ML	Tue Jan 31 00:39:40 2006 +0100
     5.3 @@ -42,28 +42,32 @@
     5.4        xprods: xprod list,
     5.5        consts: string list,
     5.6        prmodes: string list,
     5.7 -      parse_ast_translation: (string * ((theory -> Ast.ast list -> Ast.ast) * stamp)) list,
     5.8 +      parse_ast_translation:
     5.9 +        (string * ((Context.generic -> Ast.ast list -> Ast.ast) * stamp)) list,
    5.10        parse_rules: (Ast.ast * Ast.ast) list,
    5.11 -      parse_translation: (string * ((theory -> term list -> term) * stamp)) list,
    5.12 -      print_translation: (string * ((theory -> bool -> typ -> term list -> term) * stamp)) list,
    5.13 +      parse_translation:
    5.14 +        (string * ((Context.generic -> term list -> term) * stamp)) list,
    5.15 +      print_translation:
    5.16 +        (string * ((Context.generic -> bool -> typ -> term list -> term) * stamp)) list,
    5.17        print_rules: (Ast.ast * Ast.ast) list,
    5.18 -      print_ast_translation: (string * ((theory -> Ast.ast list -> Ast.ast) * stamp)) list,
    5.19 +      print_ast_translation:
    5.20 +        (string * ((Context.generic -> Ast.ast list -> Ast.ast) * stamp)) list,
    5.21        token_translation: (string * string * (string -> string * real)) list}
    5.22    val mfix_args: string -> int
    5.23    val escape_mfix: string -> string
    5.24    val unlocalize_mfix: string -> string
    5.25    val syn_ext': bool -> (string -> bool) -> mfix list ->
    5.26 -    string list -> (string * ((theory -> Ast.ast list -> Ast.ast) * stamp)) list *
    5.27 -    (string * ((theory -> term list -> term) * stamp)) list *
    5.28 -    (string * ((theory -> bool -> typ -> term list -> term) * stamp)) list *
    5.29 -    (string * ((theory -> Ast.ast list -> Ast.ast) * stamp)) list
    5.30 +    string list -> (string * ((Context.generic -> Ast.ast list -> Ast.ast) * stamp)) list *
    5.31 +    (string * ((Context.generic -> term list -> term) * stamp)) list *
    5.32 +    (string * ((Context.generic -> bool -> typ -> term list -> term) * stamp)) list *
    5.33 +    (string * ((Context.generic -> Ast.ast list -> Ast.ast) * stamp)) list
    5.34      -> (string * string * (string -> string * real)) list
    5.35      -> (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext
    5.36    val syn_ext: mfix list -> string list ->
    5.37 -    (string * ((theory -> Ast.ast list -> Ast.ast) * stamp)) list *
    5.38 -    (string * ((theory -> term list -> term) * stamp)) list *
    5.39 -    (string * ((theory -> bool -> typ -> term list -> term) * stamp)) list *
    5.40 -    (string * ((theory -> Ast.ast list -> Ast.ast) * stamp)) list
    5.41 +    (string * ((Context.generic -> Ast.ast list -> Ast.ast) * stamp)) list *
    5.42 +    (string * ((Context.generic -> term list -> term) * stamp)) list *
    5.43 +    (string * ((Context.generic -> bool -> typ -> term list -> term) * stamp)) list *
    5.44 +    (string * ((Context.generic -> Ast.ast list -> Ast.ast) * stamp)) list
    5.45      -> (string * string * (string -> string * real)) list
    5.46      -> (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext
    5.47    val syn_ext_const_names: string list -> syn_ext
    5.48 @@ -74,10 +78,10 @@
    5.49      (string * ((bool -> typ -> term list -> term) * stamp)) list *
    5.50      (string * ((Ast.ast list -> Ast.ast) * stamp)) list -> syn_ext
    5.51    val syn_ext_advanced_trfuns:
    5.52 -    (string * ((theory -> Ast.ast list -> Ast.ast) * stamp)) list *
    5.53 -    (string * ((theory -> term list -> term) * stamp)) list *
    5.54 -    (string * ((theory -> bool -> typ -> term list -> term) * stamp)) list *
    5.55 -    (string * ((theory -> Ast.ast list -> Ast.ast) * stamp)) list -> syn_ext
    5.56 +    (string * ((Context.generic -> Ast.ast list -> Ast.ast) * stamp)) list *
    5.57 +    (string * ((Context.generic -> term list -> term) * stamp)) list *
    5.58 +    (string * ((Context.generic -> bool -> typ -> term list -> term) * stamp)) list *
    5.59 +    (string * ((Context.generic -> Ast.ast list -> Ast.ast) * stamp)) list -> syn_ext
    5.60    val syn_ext_tokentrfuns: (string * string * (string -> string * real)) list -> syn_ext
    5.61    val standard_token_markers: string list
    5.62    val pure_ext: syn_ext
    5.63 @@ -336,12 +340,16 @@
    5.64      xprods: xprod list,
    5.65      consts: string list,
    5.66      prmodes: string list,
    5.67 -    parse_ast_translation: (string * ((theory -> Ast.ast list -> Ast.ast) * stamp)) list,
    5.68 +    parse_ast_translation:
    5.69 +      (string * ((Context.generic -> Ast.ast list -> Ast.ast) * stamp)) list,
    5.70      parse_rules: (Ast.ast * Ast.ast) list,
    5.71 -    parse_translation: (string * ((theory -> term list -> term) * stamp)) list,
    5.72 -    print_translation: (string * ((theory -> bool -> typ -> term list -> term) * stamp)) list,
    5.73 +    parse_translation:
    5.74 +      (string * ((Context.generic -> term list -> term) * stamp)) list,
    5.75 +    print_translation:
    5.76 +      (string * ((Context.generic -> bool -> typ -> term list -> term) * stamp)) list,
    5.77      print_rules: (Ast.ast * Ast.ast) list,
    5.78 -    print_ast_translation: (string * ((theory -> Ast.ast list -> Ast.ast) * stamp)) list,
    5.79 +    print_ast_translation:
    5.80 +      (string * ((Context.generic -> Ast.ast list -> Ast.ast) * stamp)) list,
    5.81      token_translation: (string * string * (string -> string * real)) list};
    5.82  
    5.83  
     6.1 --- a/src/Pure/Syntax/syn_trans.ML	Mon Jan 30 15:31:31 2006 +0100
     6.2 +++ b/src/Pure/Syntax/syn_trans.ML	Tue Jan 31 00:39:40 2006 +0100
     6.3 @@ -50,10 +50,11 @@
     6.4    val prop_tr': term -> term
     6.5    val appl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
     6.6    val applC_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
     6.7 -  val pts_to_asts: theory -> (string -> (theory -> Ast.ast list -> Ast.ast) option) ->
     6.8 +  val pts_to_asts: Context.generic ->
     6.9 +    (string -> (Context.generic -> Ast.ast list -> Ast.ast) option) ->
    6.10      Parser.parsetree list -> Ast.ast list
    6.11 -  val asts_to_terms: theory -> (string -> (theory -> term list -> term) option) ->
    6.12 -    Ast.ast list -> term list
    6.13 +  val asts_to_terms: Context.generic ->
    6.14 +    (string -> (Context.generic -> term list -> term) option) -> Ast.ast list -> term list
    6.15  end;
    6.16  
    6.17  structure SynTrans: SYN_TRANS =
    6.18 @@ -460,14 +461,14 @@
    6.19  
    6.20  (** pts_to_asts **)
    6.21  
    6.22 -fun pts_to_asts thy trf pts =
    6.23 +fun pts_to_asts context trf pts =
    6.24    let
    6.25      fun trans a args =
    6.26        (case trf a of
    6.27          NONE => Ast.mk_appl (Ast.Constant a) args
    6.28        | SOME f => transform_failure (fn exn =>
    6.29              EXCEPTION (exn, "Error in parse ast translation for " ^ quote a))
    6.30 -          (fn () => f thy args) ());
    6.31 +          (fn () => f context args) ());
    6.32  
    6.33      (*translate pt bottom-up*)
    6.34      fun ast_of (Parser.Node (a, pts)) = trans a (map ast_of pts)
    6.35 @@ -484,14 +485,14 @@
    6.36  
    6.37  val fixedN = "\\<^fixed>";
    6.38  
    6.39 -fun asts_to_terms thy trf asts =
    6.40 +fun asts_to_terms context trf asts =
    6.41    let
    6.42      fun trans a args =
    6.43        (case trf a of
    6.44          NONE => Term.list_comb (Lexicon.const a, args)
    6.45        | SOME f => transform_failure (fn exn =>
    6.46              EXCEPTION (exn, "Error in parse translation for " ^ quote a))
    6.47 -          (fn () => f thy args) ());
    6.48 +          (fn () => f context args) ());
    6.49  
    6.50      fun term_of (Ast.Constant a) = trans a []
    6.51        | term_of (Ast.Variable x) = Lexicon.read_var x
     7.1 --- a/src/Pure/Syntax/syntax.ML	Mon Jan 30 15:31:31 2006 +0100
     7.2 +++ b/src/Pure/Syntax/syntax.ML	Tue Jan 31 00:39:40 2006 +0100
     7.3 @@ -48,13 +48,13 @@
     7.4      (string * ((bool -> typ -> term list -> term) * stamp)) list *
     7.5      (string * ((ast list -> ast) * stamp)) list -> syntax -> syntax
     7.6    val extend_advanced_trfuns:
     7.7 -    (string * ((theory -> ast list -> ast) * stamp)) list *
     7.8 -    (string * ((theory -> term list -> term) * stamp)) list *
     7.9 -    (string * ((theory -> bool -> typ -> term list -> term) * stamp)) list *
    7.10 -    (string * ((theory -> ast list -> ast) * stamp)) list -> syntax -> syntax
    7.11 +    (string * ((Context.generic -> ast list -> ast) * stamp)) list *
    7.12 +    (string * ((Context.generic -> term list -> term) * stamp)) list *
    7.13 +    (string * ((Context.generic -> bool -> typ -> term list -> term) * stamp)) list *
    7.14 +    (string * ((Context.generic -> ast list -> ast) * stamp)) list -> syntax -> syntax
    7.15    val extend_tokentrfuns: (string * string * (string -> string * real)) list -> syntax -> syntax
    7.16    val extend_trrules_i: ast trrule list -> syntax -> syntax
    7.17 -  val extend_trrules: theory -> (string -> bool) -> syntax ->
    7.18 +  val extend_trrules: Context.generic -> (string -> bool) -> syntax ->
    7.19      (string * string) trrule list -> syntax -> syntax
    7.20    val remove_const_gram: (string -> bool) ->
    7.21      string * bool -> (string * typ * mixfix) list -> syntax -> syntax
    7.22 @@ -67,13 +67,13 @@
    7.23    val print_gram: syntax -> unit
    7.24    val print_trans: syntax -> unit
    7.25    val print_syntax: syntax -> unit
    7.26 -  val read: theory -> (string -> bool) -> syntax -> typ -> string -> term list
    7.27 -  val read_typ: theory -> syntax -> ((indexname * sort) list -> indexname -> sort) ->
    7.28 +  val read: Context.generic -> (string -> bool) -> syntax -> typ -> string -> term list
    7.29 +  val read_typ: Context.generic -> syntax -> ((indexname * sort) list -> indexname -> sort) ->
    7.30      (sort -> sort) -> string -> typ
    7.31 -  val read_sort: theory -> syntax -> string -> sort
    7.32 -  val pretty_term: theory -> syntax -> bool -> term -> Pretty.T
    7.33 -  val pretty_typ: theory -> syntax -> typ -> Pretty.T
    7.34 -  val pretty_sort: theory -> syntax -> sort -> Pretty.T
    7.35 +  val read_sort: Context.generic -> syntax -> string -> sort
    7.36 +  val pretty_term: Context.generic -> syntax -> bool -> term -> Pretty.T
    7.37 +  val pretty_typ: Context.generic -> syntax -> typ -> Pretty.T
    7.38 +  val pretty_sort: Context.generic -> syntax -> sort -> Pretty.T
    7.39    val ambiguity_level: int ref
    7.40    val ambiguity_is_error: bool ref
    7.41  end;
    7.42 @@ -169,12 +169,12 @@
    7.43      gram: Parser.gram,
    7.44      consts: string list,
    7.45      prmodes: string list,
    7.46 -    parse_ast_trtab: ((theory -> Ast.ast list -> Ast.ast) * stamp) Symtab.table,
    7.47 +    parse_ast_trtab: ((Context.generic -> Ast.ast list -> Ast.ast) * stamp) Symtab.table,
    7.48      parse_ruletab: ruletab,
    7.49 -    parse_trtab: ((theory -> term list -> term) * stamp) Symtab.table,
    7.50 -    print_trtab: ((theory -> bool -> typ -> term list -> term) * stamp) list Symtab.table,
    7.51 +    parse_trtab: ((Context.generic -> term list -> term) * stamp) Symtab.table,
    7.52 +    print_trtab: ((Context.generic -> bool -> typ -> term list -> term) * stamp) list Symtab.table,
    7.53      print_ruletab: ruletab,
    7.54 -    print_ast_trtab: ((theory -> Ast.ast list -> Ast.ast) * stamp) list Symtab.table,
    7.55 +    print_ast_trtab: ((Context.generic -> Ast.ast list -> Ast.ast) * stamp) list Symtab.table,
    7.56      tokentrtab: (string * (string * ((string -> string * real) * stamp)) list) list,
    7.57      prtabs: Printer.prtabs} * stamp;
    7.58  
    7.59 @@ -376,7 +376,7 @@
    7.60  val ambiguity_level = ref 1;
    7.61  val ambiguity_is_error = ref false
    7.62  
    7.63 -fun read_asts thy is_logtype (Syntax (tabs, _)) xids root str =
    7.64 +fun read_asts context is_logtype (Syntax (tabs, _)) xids root str =
    7.65    let
    7.66      val {lexicon, gram, parse_ast_trtab, ...} = tabs;
    7.67      val root' = if root <> "prop" andalso is_logtype root then SynExt.logic else root;
    7.68 @@ -384,41 +384,41 @@
    7.69      val pts = Parser.parse gram root' (Lexicon.tokenize lexicon xids chars);
    7.70  
    7.71      fun show_pt pt =
    7.72 -      Pretty.string_of (Ast.pretty_ast (hd (SynTrans.pts_to_asts thy (K NONE) [pt])));
    7.73 +      Pretty.string_of (Ast.pretty_ast (hd (SynTrans.pts_to_asts context (K NONE) [pt])));
    7.74    in
    7.75      conditional (length pts > ! ambiguity_level) (fn () =>
    7.76        if ! ambiguity_is_error then error ("Ambiguous input " ^ quote str)
    7.77        else (warning ("Ambiguous input " ^ quote str ^ "\n" ^
    7.78            "produces " ^ string_of_int (length pts) ^ " parse trees.");
    7.79           List.app (warning o show_pt) pts));
    7.80 -    SynTrans.pts_to_asts thy (lookup_tr parse_ast_trtab) pts
    7.81 +    SynTrans.pts_to_asts context (lookup_tr parse_ast_trtab) pts
    7.82    end;
    7.83  
    7.84  
    7.85  (* read *)
    7.86  
    7.87 -fun read thy is_logtype (syn as Syntax (tabs, _)) ty str =
    7.88 +fun read context is_logtype (syn as Syntax (tabs, _)) ty str =
    7.89    let
    7.90      val {parse_ruletab, parse_trtab, ...} = tabs;
    7.91 -    val asts = read_asts thy is_logtype syn false (SynExt.typ_to_nonterm ty) str;
    7.92 +    val asts = read_asts context is_logtype syn false (SynExt.typ_to_nonterm ty) str;
    7.93    in
    7.94 -    SynTrans.asts_to_terms thy (lookup_tr parse_trtab)
    7.95 +    SynTrans.asts_to_terms context (lookup_tr parse_trtab)
    7.96        (map (Ast.normalize_ast (Symtab.lookup_multi parse_ruletab)) asts)
    7.97    end;
    7.98  
    7.99  
   7.100  (* read types *)
   7.101  
   7.102 -fun read_typ thy syn get_sort map_sort str =
   7.103 -  (case read thy (K false) syn SynExt.typeT str of
   7.104 +fun read_typ context syn get_sort map_sort str =
   7.105 +  (case read context (K false) syn SynExt.typeT str of
   7.106      [t] => TypeExt.typ_of_term (get_sort (TypeExt.raw_term_sorts t)) map_sort t
   7.107    | _ => error "read_typ: ambiguous syntax");
   7.108  
   7.109  
   7.110  (* read sorts *)
   7.111  
   7.112 -fun read_sort thy syn str =
   7.113 -  (case read thy (K false) syn TypeExt.sortT str of
   7.114 +fun read_sort context syn str =
   7.115 +  (case read context (K false) syn TypeExt.sortT str of
   7.116      [t] => TypeExt.sort_of_term t
   7.117    | _ => error "read_sort: ambiguous syntax");
   7.118  
   7.119 @@ -452,7 +452,7 @@
   7.120    | NONE => rule);
   7.121  
   7.122  
   7.123 -fun read_pattern thy is_logtype syn (root, str) =
   7.124 +fun read_pattern context is_logtype syn (root, str) =
   7.125    let
   7.126      val Syntax ({consts, ...}, _) = syn;
   7.127  
   7.128 @@ -462,7 +462,7 @@
   7.129            else ast
   7.130        | constify (Ast.Appl asts) = Ast.Appl (map constify asts);
   7.131    in
   7.132 -    (case read_asts thy is_logtype syn true root str of
   7.133 +    (case read_asts context is_logtype syn true root str of
   7.134        [ast] => constify ast
   7.135      | _ => error ("Syntactically ambiguous input: " ^ quote str))
   7.136    end handle ERROR msg =>
   7.137 @@ -480,19 +480,19 @@
   7.138  
   7.139  (** pretty terms, typs, sorts **)
   7.140  
   7.141 -fun pretty_t t_to_ast prt_t thy (syn as Syntax (tabs, _)) curried t =
   7.142 +fun pretty_t t_to_ast prt_t context (syn as Syntax (tabs, _)) curried t =
   7.143    let
   7.144      val {print_trtab, print_ruletab, print_ast_trtab, tokentrtab, prtabs, ...} = tabs;
   7.145 -    val ast = t_to_ast thy (lookup_tr' print_trtab) t;
   7.146 +    val ast = t_to_ast context (lookup_tr' print_trtab) t;
   7.147    in
   7.148 -    prt_t thy curried prtabs (lookup_tr' print_ast_trtab)
   7.149 +    prt_t context curried prtabs (lookup_tr' print_ast_trtab)
   7.150        (lookup_tokentr tokentrtab (! print_mode))
   7.151        (Ast.normalize_ast (Symtab.lookup_multi print_ruletab) ast)
   7.152    end;
   7.153  
   7.154  val pretty_term = pretty_t Printer.term_to_ast Printer.pretty_term_ast;
   7.155 -fun pretty_typ thy syn = pretty_t Printer.typ_to_ast Printer.pretty_typ_ast thy syn false;
   7.156 -fun pretty_sort thy syn = pretty_t Printer.sort_to_ast Printer.pretty_typ_ast thy syn false;
   7.157 +fun pretty_typ context syn = pretty_t Printer.typ_to_ast Printer.pretty_typ_ast context syn false;
   7.158 +fun pretty_sort context syn = pretty_t Printer.sort_to_ast Printer.pretty_typ_ast context syn false;
   7.159  
   7.160  
   7.161  
   7.162 @@ -509,9 +509,9 @@
   7.163  val extend_tokentrfuns     = ext_syntax SynExt.syn_ext_tokentrfuns;
   7.164  val extend_trrules_i       = ext_syntax SynExt.syn_ext_rules o prep_rules I;
   7.165  
   7.166 -fun extend_trrules thy is_logtype syn rules =
   7.167 +fun extend_trrules context is_logtype syn rules =
   7.168    ext_syntax' (K SynExt.syn_ext_rules) (K false) default_mode
   7.169 -    (prep_rules (read_pattern thy is_logtype syn) rules);
   7.170 +    (prep_rules (read_pattern context is_logtype syn) rules);
   7.171  
   7.172  fun remove_const_gram is_logtype prmode decls =
   7.173    remove_syntax prmode (Mixfix.syn_ext_consts is_logtype decls);
     8.1 --- a/src/Pure/sign.ML	Mon Jan 30 15:31:31 2006 +0100
     8.2 +++ b/src/Pure/sign.ML	Tue Jan 31 00:39:40 2006 +0100
     8.3 @@ -39,12 +39,12 @@
     8.4    val add_trfunsT:
     8.5      (string * (bool -> typ -> term list -> term)) list -> theory -> theory
     8.6    val add_advanced_trfuns:
     8.7 -    (string * (theory -> ast list -> ast)) list *
     8.8 -    (string * (theory -> term list -> term)) list *
     8.9 -    (string * (theory -> term list -> term)) list *
    8.10 -    (string * (theory -> ast list -> ast)) list -> theory -> theory
    8.11 +    (string * (Context.generic -> ast list -> ast)) list *
    8.12 +    (string * (Context.generic -> term list -> term)) list *
    8.13 +    (string * (Context.generic -> term list -> term)) list *
    8.14 +    (string * (Context.generic -> ast list -> ast)) list -> theory -> theory
    8.15    val add_advanced_trfunsT:
    8.16 -    (string * (theory -> bool -> typ -> term list -> term)) list -> theory -> theory
    8.17 +    (string * (Context.generic -> bool -> typ -> term list -> term)) list -> theory -> theory
    8.18    val add_tokentrfuns:
    8.19      (string * string * (string -> string * real)) list -> theory -> theory
    8.20    val add_mode_tokentrfuns: string -> (string * (string -> string * real)) list
    8.21 @@ -132,7 +132,7 @@
    8.22    val intern_term: theory -> term -> term
    8.23    val extern_term: theory -> term -> term
    8.24    val intern_tycons: theory -> typ -> typ
    8.25 -  val pretty_term': Syntax.syntax -> theory -> term -> Pretty.T
    8.26 +  val pretty_term': Syntax.syntax -> Context.generic -> term -> Pretty.T
    8.27    val pretty_term: theory -> term -> Pretty.T
    8.28    val pretty_typ: theory -> typ -> Pretty.T
    8.29    val pretty_sort: theory -> sort -> Pretty.T
    8.30 @@ -155,11 +155,14 @@
    8.31    val certify_prop: Pretty.pp -> theory -> term -> term * typ * int
    8.32    val cert_term: theory -> term -> term
    8.33    val cert_prop: theory -> term -> term
    8.34 -  val read_sort': Syntax.syntax -> theory -> string -> sort
    8.35 +  val read_sort': Syntax.syntax -> Context.generic -> string -> sort
    8.36    val read_sort: theory -> string -> sort
    8.37 -  val read_typ': Syntax.syntax -> theory * (indexname -> sort option) -> string -> typ
    8.38 -  val read_typ_syntax': Syntax.syntax -> theory * (indexname -> sort option) -> string -> typ
    8.39 -  val read_typ_abbrev': Syntax.syntax -> theory * (indexname -> sort option) -> string -> typ
    8.40 +  val read_typ': Syntax.syntax -> Context.generic ->
    8.41 +    (indexname -> sort option) -> string -> typ
    8.42 +  val read_typ_syntax': Syntax.syntax -> Context.generic ->
    8.43 +    (indexname -> sort option) -> string -> typ
    8.44 +  val read_typ_abbrev': Syntax.syntax -> Context.generic ->
    8.45 +    (indexname -> sort option) -> string -> typ
    8.46    val read_typ: theory * (indexname -> sort option) -> string -> typ
    8.47    val read_typ_syntax: theory * (indexname -> sort option) -> string -> typ
    8.48    val read_typ_abbrev: theory * (indexname -> sort option) -> string -> typ
    8.49 @@ -171,8 +174,8 @@
    8.50    val infer_types: Pretty.pp -> theory -> (indexname -> typ option) ->
    8.51      (indexname -> sort option) -> string list -> bool
    8.52      -> term list * typ -> term * (indexname * typ) list
    8.53 -  val read_def_terms': Pretty.pp -> (string -> bool) -> Syntax.syntax ->
    8.54 -    theory * (indexname -> typ option) * (indexname -> sort option) ->
    8.55 +  val read_def_terms': Pretty.pp -> (string -> bool) -> Syntax.syntax -> Context.generic ->
    8.56 +    (indexname -> typ option) * (indexname -> sort option) ->
    8.57      string list -> bool -> (string * typ) list -> term list * (indexname * typ) list
    8.58    val read_def_terms:
    8.59      theory * (indexname -> typ option) * (indexname -> sort option) ->
    8.60 @@ -338,11 +341,16 @@
    8.61  
    8.62  (** pretty printing of terms, types etc. **)
    8.63  
    8.64 -fun pretty_term' syn thy t =
    8.65 -  Syntax.pretty_term thy syn (Context.exists_name Context.CPureN thy) (extern_term thy t);
    8.66 -fun pretty_term thy t = pretty_term' (syn_of thy) thy t;
    8.67 -fun pretty_typ thy T = Syntax.pretty_typ thy (syn_of thy) (extern_typ thy T);
    8.68 -fun pretty_sort thy S = Syntax.pretty_sort thy (syn_of thy) (extern_sort thy S);
    8.69 +fun pretty_term' syn context t =
    8.70 +  let
    8.71 +    val thy = Context.theory_of context;
    8.72 +    val curried = Context.exists_name Context.CPureN thy;
    8.73 +  in Syntax.pretty_term context syn curried (extern_term thy t) end;
    8.74 +
    8.75 +fun pretty_term thy t = pretty_term' (syn_of thy) (Context.Theory thy) t;
    8.76 +
    8.77 +fun pretty_typ thy T = Syntax.pretty_typ (Context.Theory thy) (syn_of thy) (extern_typ thy T);
    8.78 +fun pretty_sort thy S = Syntax.pretty_sort (Context.Theory thy) (syn_of thy) (extern_sort thy S);
    8.79  
    8.80  fun pretty_classrel thy cs = Pretty.block (List.concat
    8.81    (separate [Pretty.str " <", Pretty.brk 1] (map (single o pretty_sort thy o single) cs)));
    8.82 @@ -458,29 +466,31 @@
    8.83  
    8.84  (* sorts *)
    8.85  
    8.86 -fun read_sort' syn thy str =
    8.87 +fun read_sort' syn context str =
    8.88    let
    8.89 +    val thy = Context.theory_of context;
    8.90      val _ = Context.check_thy thy;
    8.91 -    val S = intern_sort thy (Syntax.read_sort thy syn str);
    8.92 +    val S = intern_sort thy (Syntax.read_sort context syn str);
    8.93    in certify_sort thy S handle TYPE (msg, _, _) => error msg end;
    8.94  
    8.95 -fun read_sort thy str = read_sort' (syn_of thy) thy str;
    8.96 +fun read_sort thy str = read_sort' (syn_of thy) (Context.Theory thy) str;
    8.97  
    8.98  
    8.99  (* types *)
   8.100  
   8.101  local
   8.102  
   8.103 -fun gen_read_typ' cert syn (thy, def_sort) str =
   8.104 +fun gen_read_typ' cert syn context def_sort str =
   8.105    let
   8.106 +    val thy = Context.theory_of context;
   8.107      val _ = Context.check_thy thy;
   8.108      val get_sort = TypeInfer.get_sort (tsig_of thy) def_sort (intern_sort thy);
   8.109 -    val T = intern_tycons thy (Syntax.read_typ thy syn get_sort (intern_sort thy) str);
   8.110 +    val T = intern_tycons thy (Syntax.read_typ context syn get_sort (intern_sort thy) str);
   8.111    in cert thy T handle TYPE (msg, _, _) => error msg end
   8.112    handle ERROR msg => cat_error msg ("The error(s) above occurred in type " ^ quote str);
   8.113  
   8.114  fun gen_read_typ cert (thy, def_sort) str =
   8.115 -  gen_read_typ' cert (syn_of thy) (thy, def_sort) str;
   8.116 +  gen_read_typ' cert (syn_of thy) (Context.Theory thy) def_sort str;
   8.117  
   8.118  in
   8.119  
   8.120 @@ -563,15 +573,16 @@
   8.121  
   8.122  (* read_def_terms -- read terms and infer types *)    (*exception ERROR*)
   8.123  
   8.124 -fun read_def_terms' pp is_logtype syn (thy, types, sorts) used freeze sTs =
   8.125 +fun read_def_terms' pp is_logtype syn context (types, sorts) used freeze sTs =
   8.126    let
   8.127 +    val thy = Context.theory_of context;
   8.128      fun read (s, T) =
   8.129        let val T' = certify_typ thy T handle TYPE (msg, _, _) => error msg
   8.130 -      in (Syntax.read thy is_logtype syn T' s, T') end;
   8.131 +      in (Syntax.read context is_logtype syn T' s, T') end;
   8.132    in infer_types_simult pp thy types sorts used freeze (map read sTs) end;
   8.133  
   8.134  fun read_def_terms (thy, types, sorts) =
   8.135 -  read_def_terms' (pp thy) (is_logtype thy) (syn_of thy) (thy, types, sorts);
   8.136 +  read_def_terms' (pp thy) (is_logtype thy) (syn_of thy) (Context.Theory thy) (types, sorts);
   8.137  
   8.138  fun simple_read_term thy T s =
   8.139    let val ([t], _) = read_def_terms (thy, K NONE, K NONE) [] true [(s, T)]
   8.140 @@ -770,7 +781,7 @@
   8.141  local
   8.142  
   8.143  fun advancedT false = ""
   8.144 -  | advancedT true = "theory -> ";
   8.145 +  | advancedT true = "Context.generic -> ";
   8.146  
   8.147  fun advancedN false = ""
   8.148    | advancedN true = "advanced_";
   8.149 @@ -813,7 +824,7 @@
   8.150  
   8.151  fun add_trrules args thy = thy |> map_syn (fn syn =>
   8.152    let val rules = map (Syntax.map_trrule (apfst (intern_type thy))) args
   8.153 -  in Syntax.extend_trrules thy (is_logtype thy) syn rules syn end);
   8.154 +  in Syntax.extend_trrules (Context.Theory thy) (is_logtype thy) syn rules syn end);
   8.155  
   8.156  val add_trrules_i = map_syn o Syntax.extend_trrules_i;
   8.157  
     9.1 --- a/src/Pure/theory.ML	Mon Jan 30 15:31:31 2006 +0100
     9.2 +++ b/src/Pure/theory.ML	Tue Jan 31 00:39:40 2006 +0100
     9.3 @@ -187,7 +187,7 @@
     9.4  
     9.5  fun read_def_axm (thy, types, sorts) used (name, str) =
     9.6    let
     9.7 -    val ts = Syntax.read thy (Sign.is_logtype thy) (Sign.syn_of thy) propT str;
     9.8 +    val ts = Syntax.read (Context.Theory thy) (Sign.is_logtype thy) (Sign.syn_of thy) propT str;
     9.9      val (t, _) = Sign.infer_types (Sign.pp thy) thy types sorts used true (ts, propT);
    9.10    in cert_axm thy (name, t) end
    9.11    handle ERROR msg => err_in_axm msg name;