# HG changeset patch
# User wenzelm
# Date 1267132653 -3600
# Node ID 09489d8ffece4bce4c165300eb05b466cdba6831
# Parent  828a42fb74453e819b9eb2217a6090f667d07651
explicit @{type_syntax} markup;

diff -r 828a42fb7445 -r 09489d8ffece src/HOL/Tools/Datatype/datatype_case.ML
--- 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});
 
 
 (*---------------------------------------------------------------------------
diff -r 828a42fb7445 -r 09489d8ffece src/HOL/Tools/numeral_syntax.ML
--- 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
diff -r 828a42fb7445 -r 09489d8ffece src/HOL/Tools/record.ML
--- 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
diff -r 828a42fb7445 -r 09489d8ffece src/HOL/Tools/string_syntax.ML
--- 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);
 
diff -r 828a42fb7445 -r 09489d8ffece src/HOL/Typerep.thy
--- 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;
diff -r 828a42fb7445 -r 09489d8ffece src/HOL/ex/Numeral.thy
--- 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
diff -r 828a42fb7445 -r 09489d8ffece src/Sequents/Sequents.thy
--- 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