equal
deleted
inserted
replaced
142 (case Thm.term_of ct of |
142 (case Thm.term_of ct of |
143 Const (@{const_name HOL.eq}, _) $ _ $ _ => Thm.dest_binop ct |
143 Const (@{const_name HOL.eq}, _) $ _ $ _ => Thm.dest_binop ct |
144 | @{const HOL.implies} $ _ $ _ => dest_cond_eq (Thm.dest_arg ct) |
144 | @{const HOL.implies} $ _ $ _ => dest_cond_eq (Thm.dest_arg ct) |
145 | _ => raise CTERM ("no equation", [ct])) |
145 | _ => raise CTERM ("no equation", [ct])) |
146 |
146 |
147 fun get_constrs thy (Type (n, _)) = these (Datatype.get_constrs thy n) |
147 fun get_constrs thy (Type (n, _)) = these (Datatype_Data.get_constrs thy n) |
148 | get_constrs _ _ = [] |
148 | get_constrs _ _ = [] |
149 |
149 |
150 fun is_constr thy (n, T) = |
150 fun is_constr thy (n, T) = |
151 let fun match (m, U) = m = n andalso Sign.typ_instance thy (T, U) |
151 let fun match (m, U) = m = n andalso Sign.typ_instance thy (T, U) |
152 in can (the o find_first match o get_constrs thy o Term.body_type) T end |
152 in can (the o find_first match o get_constrs thy o Term.body_type) T end |