equal
deleted
inserted
replaced
543 | NONE => bad_thm ("Not an abstract type: " ^ tyco); |
543 | NONE => bad_thm ("Not an abstract type: " ^ tyco); |
544 val _ = if rep_const = rep' then () |
544 val _ = if rep_const = rep' then () |
545 else bad_thm ("Projection mismatch: " ^ quote rep_const ^ " vs. " ^ quote rep'); |
545 else bad_thm ("Projection mismatch: " ^ quote rep_const ^ " vs. " ^ quote rep'); |
546 val _ = check_eqn thy { allow_nonlinear = false, |
546 val _ = check_eqn thy { allow_nonlinear = false, |
547 allow_consts = false, allow_pats = false } thm (lhs, rhs); |
547 allow_consts = false, allow_pats = false } thm (lhs, rhs); |
548 val _ = if forall2 (fn T => fn (_, sort) => Sign.of_sort thy (T, sort)) Ts vs' then () |
548 val _ = if ListPair.all (fn (T, (_, sort)) => Sign.of_sort thy (T, sort)) (Ts, vs') then () |
549 else error ("Type arguments do not satisfy sort constraints of abstype certificate."); |
549 else error ("Type arguments do not satisfy sort constraints of abstype certificate."); |
550 in (thm, tyco) end; |
550 in (thm, tyco) end; |
551 |
551 |
552 fun assert_eqn thy = gen_assert_eqn thy true; |
552 fun assert_eqn thy = gen_assert_eqn thy true; |
553 |
553 |