equal
deleted
inserted
replaced
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 |