src/HOL/Num.thy
changeset 49690 a6814de45b69
parent 48891 c0eafbd55de3
child 49962 a8cc904a6820
     1.1 --- a/src/HOL/Num.thy	Wed Oct 03 16:59:20 2012 +0200
     1.2 +++ b/src/HOL/Num.thy	Wed Oct 03 16:59:58 2012 +0200
     1.3 @@ -323,7 +323,7 @@
     1.4      in
     1.5        case T of
     1.6          Type (@{type_name fun}, [_, T']) =>
     1.7 -          if not (Config.get ctxt show_types) andalso can Term.dest_Type T' then t'
     1.8 +          if not (Printer.show_type_constraint ctxt) andalso can Term.dest_Type T' then t'
     1.9            else Syntax.const @{syntax_const "_constrain"} $ t' $ Syntax_Phases.term_of_typ ctxt T'
    1.10        | T' => if T' = dummyT then t' else raise Match
    1.11      end;