equal
deleted
inserted
replaced
128 let |
128 let |
129 fun tr' c = (c, fn ctxt => fn T => fn ts => |
129 fun tr' c = (c, fn ctxt => 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_Phases.term_of_typ ctxt T); |
133 else |
|
134 Syntax.const @{syntax_const "_constrain"} $ Syntax.const c $ |
|
135 Syntax_Phases.term_of_typ ctxt T); |
134 in map tr' [@{const_syntax Groups.one}, @{const_syntax Groups.zero}] end; |
136 in map tr' [@{const_syntax Groups.one}, @{const_syntax Groups.zero}] end; |
135 *} -- {* show types that are presumably too general *} |
137 *} -- {* show types that are presumably too general *} |
136 |
138 |
137 class plus = |
139 class plus = |
138 fixes plus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "+" 65) |
140 fixes plus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "+" 65) |