equal
deleted
inserted
replaced
200 val class_ctxt = begin sups base_sort (ProofContext.init_global thy); |
200 val class_ctxt = begin sups base_sort (ProofContext.init_global thy); |
201 val ((_, _, syntax_elems), _) = class_ctxt |
201 val ((_, _, syntax_elems), _) = class_ctxt |
202 |> Expression.cert_declaration supexpr I inferred_elems; |
202 |> Expression.cert_declaration supexpr I inferred_elems; |
203 fun check_vars e vs = if null vs |
203 fun check_vars e vs = if null vs |
204 then error ("No type variable in part of specification element " |
204 then error ("No type variable in part of specification element " |
205 ^ (Pretty.output o Pretty.chunks) (Element.pretty_ctxt class_ctxt e)) |
205 ^ (Pretty.output NONE o Pretty.chunks) (Element.pretty_ctxt class_ctxt e)) |
206 else (); |
206 else (); |
207 fun check_element (e as Element.Fixes fxs) = |
207 fun check_element (e as Element.Fixes fxs) = |
208 map (fn (_, SOME T, _) => check_vars e (Term.add_tfreesT T [])) fxs |
208 map (fn (_, SOME T, _) => check_vars e (Term.add_tfreesT T [])) fxs |
209 | check_element (e as Element.Assumes assms) = |
209 | check_element (e as Element.Assumes assms) = |
210 maps (fn (_, ts_pss) => map |
210 maps (fn (_, ts_pss) => map |