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