src/HOL/Tools/numeral_syntax.ML
changeset 39134 917b4b6ba3d2
parent 35430 df2862dc23a8
child 42245 29e3967550d5
     1.1 --- a/src/HOL/Tools/numeral_syntax.ML	Sun Sep 05 19:47:40 2010 +0200
     1.2 +++ b/src/HOL/Tools/numeral_syntax.ML	Sun Sep 05 21:41:24 2010 +0200
     1.3 @@ -69,15 +69,15 @@
     1.4  
     1.5  in
     1.6  
     1.7 -fun numeral_tr' show_sorts (*"number_of"*) (Type (@{type_name fun}, [_, T])) (t :: ts) =
     1.8 +fun numeral_tr' ctxt show_sorts (*"number_of"*) (Type (@{type_name 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 +        if not (Config.get ctxt show_types) andalso can Term.dest_Type T then syntax_numeral t
    1.12          else Syntax.const Syntax.constrainC $ syntax_numeral t $ Syntax.term_of_typ show_sorts T
    1.13        in list_comb (t', ts) end
    1.14 -  | numeral_tr' _ (*"number_of"*) T (t :: ts) =
    1.15 +  | numeral_tr' _ _ (*"number_of"*) T (t :: ts) =
    1.16        if T = dummyT then list_comb (syntax_numeral t, ts)
    1.17        else raise Match
    1.18 -  | numeral_tr' _ (*"number_of"*) _ _ = raise Match;
    1.19 +  | numeral_tr' _ _ (*"number_of"*) _ _ = raise Match;
    1.20  
    1.21  end;
    1.22  
    1.23 @@ -86,6 +86,6 @@
    1.24  
    1.25  val setup =
    1.26    Sign.add_trfuns ([], [(@{syntax_const "_Numeral"}, numeral_tr)], [], []) #>
    1.27 -  Sign.add_trfunsT [(@{const_syntax Int.number_of}, numeral_tr')];
    1.28 +  Sign.add_advanced_trfunsT [(@{const_syntax Int.number_of}, numeral_tr')];
    1.29  
    1.30  end;