1.1 --- a/src/HOL/Tools/numeral_syntax.ML	Wed Apr 06 13:27:59 2011 +0200
     1.2 +++ b/src/HOL/Tools/numeral_syntax.ML	Wed Apr 06 13:33:46 2011 +0200
     1.3 @@ -69,17 +69,17 @@
     1.4  
     1.5  in
     1.6  
     1.7 -fun numeral_tr' ctxt show_sorts (*"number_of"*) (Type (@{type_name fun}, [_, T])) (t :: ts) =
     1.8 +fun numeral_tr' ctxt (Type (@{type_name fun}, [_, T])) (t :: ts) =
     1.9        let val t' =
    1.10          if not (Config.get ctxt show_types) andalso can Term.dest_Type T then syntax_numeral t
    1.11          else
    1.12            Syntax.const Syntax.constrainC $ syntax_numeral t $
    1.13 -            Syntax_Phases.term_of_typ show_sorts T
    1.14 +            Syntax_Phases.term_of_typ ctxt T
    1.15        in list_comb (t', ts) end
    1.16 -  | numeral_tr' _ _ (*"number_of"*) T (t :: ts) =
    1.17 +  | numeral_tr' _ T (t :: ts) =
    1.18        if T = dummyT then list_comb (syntax_numeral t, ts)
    1.19        else raise Match
    1.20 -  | numeral_tr' _ _ (*"number_of"*) _ _ = raise Match;
    1.21 +  | numeral_tr' _ _ _ = raise Match;
    1.22  
    1.23  end;
    1.24