equal
deleted
inserted
replaced
188 fun mk_syn thy c = |
188 fun mk_syn thy c = |
189 if Syntax.is_identifier c andalso not (Syntax.is_keyword (Sign.syn_of thy) c) then NoSyn |
189 if Syntax.is_identifier c andalso not (Syntax.is_keyword (Sign.syn_of thy) c) then NoSyn |
190 else Syntax.literal c |
190 else Syntax.literal c |
191 |
191 |
192 fun quotename c = |
192 fun quotename c = |
193 if Syntax.is_identifier c andalso not (OuterSyntax.is_keyword c) then c else quote c |
193 if Syntax.is_identifier c andalso not (OuterKeyword.is_keyword c) then c else quote c |
194 |
194 |
195 fun simple_smart_string_of_cterm ct = |
195 fun simple_smart_string_of_cterm ct = |
196 let |
196 let |
197 val thy = Thm.theory_of_cterm ct; |
197 val thy = Thm.theory_of_cterm ct; |
198 val {t,T,...} = rep_cterm ct |
198 val {t,T,...} = rep_cterm ct |