explicit @{type_syntax} markup;
authorwenzelm
Thu Feb 25 22:17:33 2010 +0100 (2010-02-25)
changeset 3536309489d8ffece
parent 35362 828a42fb7445
child 35364 b8c62d60195c
explicit @{type_syntax} markup;
src/HOL/Tools/Datatype/datatype_case.ML
src/HOL/Tools/numeral_syntax.ML
src/HOL/Tools/record.ML
src/HOL/Tools/string_syntax.ML
src/HOL/Typerep.thy
src/HOL/ex/Numeral.thy
src/Sequents/Sequents.thy
     1.1 --- a/src/HOL/Tools/Datatype/datatype_case.ML	Thu Feb 25 22:15:27 2010 +0100
     1.2 +++ b/src/HOL/Tools/Datatype/datatype_case.ML	Thu Feb 25 22:17:33 2010 +0100
     1.3 @@ -76,7 +76,7 @@
     1.4  
     1.5  fun mk_fun_constrain tT t =
     1.6    Syntax.const @{syntax_const "_constrain"} $ t $
     1.7 -    (Syntax.free "fun" $ tT $ Syntax.free "dummy");    (* FIXME @{type_syntax} (!?) *)
     1.8 +    (Syntax.const @{type_syntax fun} $ tT $ Syntax.const @{type_syntax dummy});
     1.9  
    1.10  
    1.11  (*---------------------------------------------------------------------------
     2.1 --- a/src/HOL/Tools/numeral_syntax.ML	Thu Feb 25 22:15:27 2010 +0100
     2.2 +++ b/src/HOL/Tools/numeral_syntax.ML	Thu Feb 25 22:17:33 2010 +0100
     2.3 @@ -69,7 +69,7 @@
     2.4  
     2.5  in
     2.6  
     2.7 -fun numeral_tr' show_sorts (*"number_of"*) (Type ("fun", [_, T])) (t :: ts) =  (* FIXME @{type_syntax} *)
     2.8 +fun numeral_tr' show_sorts (*"number_of"*) (Type (@{type_syntax fun}, [_, T])) (t :: ts) =
     2.9        let val t' =
    2.10          if not (! show_types) andalso can Term.dest_Type T then syntax_numeral t
    2.11          else Syntax.const Syntax.constrainC $ syntax_numeral t $ Syntax.term_of_typ show_sorts T
     3.1 --- a/src/HOL/Tools/record.ML	Thu Feb 25 22:15:27 2010 +0100
     3.2 +++ b/src/HOL/Tools/record.ML	Thu Feb 25 22:17:33 2010 +0100
     3.3 @@ -762,8 +762,7 @@
     3.4      mk_ext (field_types_tr t)
     3.5    end;
     3.6  
     3.7 -(* FIXME @{type_syntax} *)
     3.8 -fun record_type_tr ctxt [t] = record_field_types_tr (Syntax.const "Product_Type.unit") ctxt t
     3.9 +fun record_type_tr ctxt [t] = record_field_types_tr (Syntax.const @{type_syntax unit}) ctxt t
    3.10    | record_type_tr _ ts = raise TERM ("record_type_tr", ts);
    3.11  
    3.12  fun record_type_scheme_tr ctxt [t, more] = record_field_types_tr more ctxt t
     4.1 --- a/src/HOL/Tools/string_syntax.ML	Thu Feb 25 22:15:27 2010 +0100
     4.2 +++ b/src/HOL/Tools/string_syntax.ML	Thu Feb 25 22:17:33 2010 +0100
     4.3 @@ -71,7 +71,7 @@
     4.4        [] =>
     4.5          Syntax.Appl
     4.6            [Syntax.Constant Syntax.constrainC,
     4.7 -            Syntax.Constant @{const_syntax Nil}, Syntax.Constant "string"]  (* FIXME @{type_syntax} *)
     4.8 +            Syntax.Constant @{const_syntax Nil}, Syntax.Constant @{type_syntax string}]
     4.9      | cs => mk_string cs)
    4.10    | string_ast_tr asts = raise AST ("string_tr", asts);
    4.11  
     5.1 --- a/src/HOL/Typerep.thy	Thu Feb 25 22:15:27 2010 +0100
     5.2 +++ b/src/HOL/Typerep.thy	Thu Feb 25 22:17:33 2010 +0100
     5.3 @@ -25,15 +25,16 @@
     5.4    fun typerep_tr (*"_TYPEREP"*) [ty] =
     5.5          Syntax.const @{const_syntax typerep} $
     5.6            (Syntax.const @{syntax_const "_constrain"} $ Syntax.const @{const_syntax "TYPE"} $
     5.7 -            (Syntax.const "itself" $ ty))  (* FIXME @{type_syntax} *)
     5.8 +            (Syntax.const @{type_syntax itself} $ ty))
     5.9      | typerep_tr (*"_TYPEREP"*) ts = raise TERM ("typerep_tr", ts);
    5.10  in [(@{syntax_const "_TYPEREP"}, typerep_tr)] end
    5.11  *}
    5.12  
    5.13  typed_print_translation {*
    5.14  let
    5.15 -  fun typerep_tr' show_sorts (*"typerep"*)  (* FIXME @{type_syntax} *)
    5.16 -          (Type ("fun", [Type ("itself", [T]), _])) (Const (@{const_syntax TYPE}, _) :: ts) =
    5.17 +  fun typerep_tr' show_sorts (*"typerep"*)
    5.18 +          (Type (@{type_syntax fun}, [Type (@{type_syntax itself}, [T]), _]))
    5.19 +          (Const (@{const_syntax TYPE}, _) :: ts) =
    5.20          Term.list_comb
    5.21            (Syntax.const @{syntax_const "_TYPEREP"} $ Syntax.term_of_typ show_sorts T, ts)
    5.22      | typerep_tr' _ T ts = raise Match;
     6.1 --- a/src/HOL/ex/Numeral.thy	Thu Feb 25 22:15:27 2010 +0100
     6.2 +++ b/src/HOL/ex/Numeral.thy	Thu Feb 25 22:17:33 2010 +0100
     6.3 @@ -327,7 +327,7 @@
     6.4        val k = int_of_num' n;
     6.5        val t' = Syntax.const @{syntax_const "_Numerals"} $ Syntax.free ("#" ^ string_of_int k);
     6.6      in case T
     6.7 -     of Type ("fun", [_, T']) =>  (* FIXME @{type_syntax} *)
     6.8 +     of Type (@{type_syntax fun}, [_, T']) =>
     6.9           if not (! show_types) andalso can Term.dest_Type T' then t'
    6.10           else Syntax.const Syntax.constrainC $ t' $ Syntax.term_of_typ show_sorts T'
    6.11        | T' => if T' = dummyT then t' else raise Match
     7.1 --- a/src/Sequents/Sequents.thy	Thu Feb 25 22:15:27 2010 +0100
     7.2 +++ b/src/Sequents/Sequents.thy	Thu Feb 25 22:17:33 2010 +0100
     7.3 @@ -65,7 +65,7 @@
     7.4  
     7.5  (* parse translation for sequences *)
     7.6  
     7.7 -fun abs_seq' t = Abs ("s", Type ("seq'", []), t);   (* FIXME @{type_syntax} *)
     7.8 +fun abs_seq' t = Abs ("s", Type (@{type_syntax seq'}, []), t);
     7.9  
    7.10  fun seqobj_tr (Const (@{syntax_const "_SeqO"}, _) $ f) =
    7.11        Const (@{const_syntax SeqO'}, dummyT) $ f