--- a/src/Pure/Syntax/syntax_phases.ML Wed Apr 06 13:27:59 2011 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML Wed Apr 06 13:33:46 2011 +0200
@@ -12,7 +12,7 @@
val decode_term: Proof.context ->
Position.reports * term Exn.result -> Position.reports * term Exn.result
val parse_ast_pattern: Proof.context -> string * string -> Ast.ast
- val term_of_typ: bool -> typ -> term
+ val term_of_typ: Proof.context -> typ -> term
end
structure Syntax_Phases: SYNTAX_PHASES =
@@ -411,8 +411,10 @@
(* term_of_typ *)
-fun term_of_typ show_sorts ty =
+fun term_of_typ ctxt ty =
let
+ val show_sorts = Config.get ctxt show_sorts;
+
fun of_sort t S =
if show_sorts then Lexicon.const "_ofsort" $ t $ term_of_sort S
else t;
@@ -444,7 +446,7 @@
(* sort_to_ast and typ_to_ast *)
-fun apply_typed x fs = map (fn f => fn ctxt => f ctxt (Config.get ctxt show_sorts) x) fs;
+fun apply_typed x fs = map (fn f => fn ctxt => f ctxt x) fs;
fun ast_of_termT ctxt trf tm =
let
@@ -463,7 +465,7 @@
in ast_of tm end;
fun sort_to_ast ctxt trf S = ast_of_termT ctxt trf (term_of_sort S);
-fun typ_to_ast ctxt trf T = ast_of_termT ctxt trf (term_of_typ (Config.get ctxt show_sorts) T);
+fun typ_to_ast ctxt trf T = ast_of_termT ctxt trf (term_of_typ ctxt T);
(* term_to_ast *)
@@ -544,7 +546,7 @@
and constrain t T =
if show_types andalso T <> dummyT then
Ast.Appl [Ast.Constant Syntax.constrainC, simple_ast_of ctxt t,
- ast_of_termT ctxt trf (term_of_typ show_sorts T)]
+ ast_of_termT ctxt trf (term_of_typ ctxt T)]
else simple_ast_of ctxt t;
in
tm
@@ -620,31 +622,31 @@
(* type propositions *)
-fun type_prop_tr' _ T [Const ("\\<^const>Pure.sort_constraint", _)] =
- Lexicon.const "_sort_constraint" $ term_of_typ true T
- | type_prop_tr' show_sorts T [t] =
- Lexicon.const "_ofclass" $ term_of_typ show_sorts T $ t
+fun type_prop_tr' ctxt T [Const ("\\<^const>Pure.sort_constraint", _)] =
+ Lexicon.const "_sort_constraint" $ term_of_typ (Config.put show_sorts true ctxt) T
+ | type_prop_tr' ctxt T [t] =
+ Lexicon.const "_ofclass" $ term_of_typ ctxt T $ t
| type_prop_tr' _ T ts = raise TYPE ("type_prop_tr'", [T], ts);
(* type reflection *)
-fun type_tr' show_sorts (Type ("itself", [T])) ts =
- Term.list_comb (Lexicon.const "_TYPE" $ term_of_typ show_sorts T, ts)
+fun type_tr' ctxt (Type ("itself", [T])) ts =
+ Term.list_comb (Lexicon.const "_TYPE" $ term_of_typ ctxt T, ts)
| type_tr' _ _ _ = raise Match;
(* type constraints *)
-fun type_constraint_tr' show_sorts (Type ("fun", [T, _])) (t :: ts) =
- Term.list_comb (Lexicon.const Syntax.constrainC $ t $ term_of_typ show_sorts T, ts)
+fun type_constraint_tr' ctxt (Type ("fun", [T, _])) (t :: ts) =
+ Term.list_comb (Lexicon.const Syntax.constrainC $ t $ term_of_typ ctxt T, ts)
| type_constraint_tr' _ _ _ = raise Match;
(* setup translations *)
val _ = Context.>> (Context.map_theory
- (Sign.add_trfunsT
+ (Sign.add_advanced_trfunsT
[("_type_prop", type_prop_tr'),
("\\<^const>TYPE", type_tr'),
("_type_constraint_", type_constraint_tr')]));