--- a/src/HOL/Tools/Datatype/datatype_case.ML Thu Feb 25 22:15:27 2010 +0100
+++ b/src/HOL/Tools/Datatype/datatype_case.ML Thu Feb 25 22:17:33 2010 +0100
@@ -76,7 +76,7 @@
fun mk_fun_constrain tT t =
Syntax.const @{syntax_const "_constrain"} $ t $
- (Syntax.free "fun" $ tT $ Syntax.free "dummy"); (* FIXME @{type_syntax} (!?) *)
+ (Syntax.const @{type_syntax fun} $ tT $ Syntax.const @{type_syntax dummy});
(*---------------------------------------------------------------------------
--- a/src/HOL/Tools/numeral_syntax.ML Thu Feb 25 22:15:27 2010 +0100
+++ b/src/HOL/Tools/numeral_syntax.ML Thu Feb 25 22:17:33 2010 +0100
@@ -69,7 +69,7 @@
in
-fun numeral_tr' show_sorts (*"number_of"*) (Type ("fun", [_, T])) (t :: ts) = (* FIXME @{type_syntax} *)
+fun numeral_tr' show_sorts (*"number_of"*) (Type (@{type_syntax fun}, [_, T])) (t :: ts) =
let val t' =
if not (! show_types) andalso can Term.dest_Type T then syntax_numeral t
else Syntax.const Syntax.constrainC $ syntax_numeral t $ Syntax.term_of_typ show_sorts T
--- a/src/HOL/Tools/record.ML Thu Feb 25 22:15:27 2010 +0100
+++ b/src/HOL/Tools/record.ML Thu Feb 25 22:17:33 2010 +0100
@@ -762,8 +762,7 @@
mk_ext (field_types_tr t)
end;
-(* FIXME @{type_syntax} *)
-fun record_type_tr ctxt [t] = record_field_types_tr (Syntax.const "Product_Type.unit") ctxt t
+fun record_type_tr ctxt [t] = record_field_types_tr (Syntax.const @{type_syntax unit}) ctxt t
| record_type_tr _ ts = raise TERM ("record_type_tr", ts);
fun record_type_scheme_tr ctxt [t, more] = record_field_types_tr more ctxt t
--- a/src/HOL/Tools/string_syntax.ML Thu Feb 25 22:15:27 2010 +0100
+++ b/src/HOL/Tools/string_syntax.ML Thu Feb 25 22:17:33 2010 +0100
@@ -71,7 +71,7 @@
[] =>
Syntax.Appl
[Syntax.Constant Syntax.constrainC,
- Syntax.Constant @{const_syntax Nil}, Syntax.Constant "string"] (* FIXME @{type_syntax} *)
+ Syntax.Constant @{const_syntax Nil}, Syntax.Constant @{type_syntax string}]
| cs => mk_string cs)
| string_ast_tr asts = raise AST ("string_tr", asts);
--- a/src/HOL/Typerep.thy Thu Feb 25 22:15:27 2010 +0100
+++ b/src/HOL/Typerep.thy Thu Feb 25 22:17:33 2010 +0100
@@ -25,15 +25,16 @@
fun typerep_tr (*"_TYPEREP"*) [ty] =
Syntax.const @{const_syntax typerep} $
(Syntax.const @{syntax_const "_constrain"} $ Syntax.const @{const_syntax "TYPE"} $
- (Syntax.const "itself" $ ty)) (* FIXME @{type_syntax} *)
+ (Syntax.const @{type_syntax itself} $ ty))
| typerep_tr (*"_TYPEREP"*) ts = raise TERM ("typerep_tr", ts);
in [(@{syntax_const "_TYPEREP"}, typerep_tr)] end
*}
typed_print_translation {*
let
- fun typerep_tr' show_sorts (*"typerep"*) (* FIXME @{type_syntax} *)
- (Type ("fun", [Type ("itself", [T]), _])) (Const (@{const_syntax TYPE}, _) :: ts) =
+ fun typerep_tr' show_sorts (*"typerep"*)
+ (Type (@{type_syntax fun}, [Type (@{type_syntax itself}, [T]), _]))
+ (Const (@{const_syntax TYPE}, _) :: ts) =
Term.list_comb
(Syntax.const @{syntax_const "_TYPEREP"} $ Syntax.term_of_typ show_sorts T, ts)
| typerep_tr' _ T ts = raise Match;
--- a/src/HOL/ex/Numeral.thy Thu Feb 25 22:15:27 2010 +0100
+++ b/src/HOL/ex/Numeral.thy Thu Feb 25 22:17:33 2010 +0100
@@ -327,7 +327,7 @@
val k = int_of_num' n;
val t' = Syntax.const @{syntax_const "_Numerals"} $ Syntax.free ("#" ^ string_of_int k);
in case T
- of Type ("fun", [_, T']) => (* FIXME @{type_syntax} *)
+ of Type (@{type_syntax fun}, [_, T']) =>
if not (! show_types) andalso can Term.dest_Type T' then t'
else Syntax.const Syntax.constrainC $ t' $ Syntax.term_of_typ show_sorts T'
| T' => if T' = dummyT then t' else raise Match
--- a/src/Sequents/Sequents.thy Thu Feb 25 22:15:27 2010 +0100
+++ b/src/Sequents/Sequents.thy Thu Feb 25 22:17:33 2010 +0100
@@ -65,7 +65,7 @@
(* parse translation for sequences *)
-fun abs_seq' t = Abs ("s", Type ("seq'", []), t); (* FIXME @{type_syntax} *)
+fun abs_seq' t = Abs ("s", Type (@{type_syntax seq'}, []), t);
fun seqobj_tr (Const (@{syntax_const "_SeqO"}, _) $ f) =
Const (@{const_syntax SeqO'}, dummyT) $ f