equal
deleted
inserted
replaced
376 fun mk_axioms cs thy = |
376 fun mk_axioms cs thy = |
377 raw_dep_axioms thy cs |
377 raw_dep_axioms thy cs |
378 |> (map o apsnd o map) (Sign.cert_prop thy) |
378 |> (map o apsnd o map) (Sign.cert_prop thy) |
379 |> rpair thy; |
379 |> rpair thy; |
380 fun add_constraint class (c, ty) = |
380 fun add_constraint class (c, ty) = |
381 Sign.add_const_constraint_i (c, SOME |
381 Sign.add_const_constraint (c, SOME |
382 (Term.map_type_tfree (fn (v, _) => TFree (v, [class])) ty)); |
382 (Term.map_type_tfree (fn (v, _) => TFree (v, [class])) ty)); |
383 in |
383 in |
384 thy |
384 thy |
385 |> Sign.add_path prefix |
385 |> Sign.add_path prefix |
386 |> fold_map add_const consts |
386 |> fold_map add_const consts |