tuned;
authorwenzelm
Mon May 27 21:00:30 2013 +0200 (2013-05-27)
changeset 521871f7b3aadec69
parent 52186 413dbb3c7251
child 52188 2da0033370a0
tuned;
src/HOL/Num.thy
     1.1 --- a/src/HOL/Num.thy	Mon May 27 18:39:21 2013 +0200
     1.2 +++ b/src/HOL/Num.thy	Mon May 27 21:00:30 2013 +0200
     1.3 @@ -326,14 +326,15 @@
     1.4      fun num_tr' sign ctxt T [n] =
     1.5        let
     1.6          val k = dest_num n;
     1.7 -        val t' = Syntax.const @{syntax_const "_Numeral"} $
     1.8 -          Syntax.free (sign ^ string_of_int k);
     1.9 +        val t' =
    1.10 +          Syntax.const @{syntax_const "_Numeral"} $
    1.11 +            Syntax.free (sign ^ string_of_int k);
    1.12        in
    1.13          (case T of
    1.14            Type (@{type_name fun}, [_, T']) =>
    1.15              if not (Printer.show_type_constraint ctxt) andalso can Term.dest_Type T' then t'
    1.16              else Syntax.const @{syntax_const "_constrain"} $ t' $ Syntax_Phases.term_of_typ ctxt T'
    1.17 -        | T' => if T' = dummyT then t' else raise Match)
    1.18 +        | _ => if T = dummyT then t' else raise Match)
    1.19        end;
    1.20    in
    1.21     [(@{const_syntax numeral}, num_tr' ""),