# 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