src/HOL/Tools/numeral_syntax.ML
changeset 35363 09489d8ffece
parent 35123 e286d5df187a
child 35430 df2862dc23a8
     1.1 --- a/src/HOL/Tools/numeral_syntax.ML	Thu Feb 25 22:15:27 2010 +0100
     1.2 +++ b/src/HOL/Tools/numeral_syntax.ML	Thu Feb 25 22:17:33 2010 +0100
     1.3 @@ -69,7 +69,7 @@
     1.4  
     1.5  in
     1.6  
     1.7 -fun numeral_tr' show_sorts (*"number_of"*) (Type ("fun", [_, T])) (t :: ts) =  (* FIXME @{type_syntax} *)
     1.8 +fun numeral_tr' show_sorts (*"number_of"*) (Type (@{type_syntax fun}, [_, T])) (t :: ts) =
     1.9        let val t' =
    1.10          if not (! show_types) andalso can Term.dest_Type T then syntax_numeral t
    1.11          else Syntax.const Syntax.constrainC $ syntax_numeral t $ Syntax.term_of_typ show_sorts T