src/HOL/HOL.thy
changeset 21179 99f546731724
parent 21151 25bd46916c12
child 21210 c17fd2df4e9e
equal deleted inserted replaced
21178:c3618fc6a6f7 21179:99f546731724
   206 translations
   206 translations
   207   (index) "\<^sub>1" => (index) "\<^bsub>\<struct>\<^esub>"
   207   (index) "\<^sub>1" => (index) "\<^bsub>\<struct>\<^esub>"
   208 
   208 
   209 typed_print_translation {*
   209 typed_print_translation {*
   210 let
   210 let
       
   211   val syntax_name = Sign.const_syntax_name (the_context ());
   211   fun tr' c = (c, fn show_sorts => fn T => fn ts =>
   212   fun tr' c = (c, fn show_sorts => fn T => fn ts =>
   212     if T = dummyT orelse not (! show_types) andalso can Term.dest_Type T then raise Match
   213     if T = dummyT orelse not (! show_types) andalso can Term.dest_Type T then raise Match
   213     else Syntax.const Syntax.constrainC $ Syntax.const c $ Syntax.term_of_typ show_sorts T);
   214     else Syntax.const Syntax.constrainC $ Syntax.const c $ Syntax.term_of_typ show_sorts T);
   214 in
   215 in map (tr' o Sign.const_syntax_name (the_context ())) ["HOL.one", "HOL.zero"] end;
   215   map (tr' o prefix Syntax.constN) ["HOL.one", "HOL.zero"]
       
   216 end;
       
   217 *} -- {* show types that are presumably too general *}
   216 *} -- {* show types that are presumably too general *}
   218 
   217 
   219 const_syntax
   218 const_syntax
   220   uminus  ("- _" [81] 80)
   219   uminus  ("- _" [81] 80)
   221 
   220