equal
deleted
inserted
replaced
128 let |
128 let |
129 fun tr' c = (c, fn ctxt => fn show_sorts => fn T => fn ts => |
129 fun tr' c = (c, fn ctxt => fn show_sorts => fn T => fn ts => |
130 if not (null ts) orelse T = dummyT |
130 if not (null ts) orelse T = dummyT |
131 orelse not (Config.get ctxt show_types) andalso can Term.dest_Type T |
131 orelse not (Config.get ctxt show_types) andalso can Term.dest_Type T |
132 then raise Match |
132 then raise Match |
133 else Syntax.const Syntax.constrainC $ Syntax.const c $ Syntax.term_of_typ show_sorts T); |
133 else Syntax.const Syntax.constrainC $ Syntax.const c $ Syntax_Phases.term_of_typ show_sorts T); |
134 in map tr' [@{const_syntax Groups.one}, @{const_syntax Groups.zero}] end; |
134 in map tr' [@{const_syntax Groups.one}, @{const_syntax Groups.zero}] end; |
135 *} -- {* show types that are presumably too general *} |
135 *} -- {* show types that are presumably too general *} |
136 |
136 |
137 class plus = |
137 class plus = |
138 fixes plus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "+" 65) |
138 fixes plus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "+" 65) |