src/HOL/Library/Old_SMT/old_smt_normalize.ML
changeset 58112 8081087096ad
parent 58058 1a0b18176548
child 59058 a78612c67ec0
equal deleted inserted replaced
58111:82db9ad610b9 58112:8081087096ad
   156     (case Thm.term_of ct of
   156     (case Thm.term_of ct of
   157       Const (@{const_name HOL.eq}, _) $ _ $ _ => Thm.dest_binop ct
   157       Const (@{const_name HOL.eq}, _) $ _ $ _ => Thm.dest_binop ct
   158     | @{const HOL.implies} $ _ $ _ => dest_cond_eq (Thm.dest_arg ct)
   158     | @{const HOL.implies} $ _ $ _ => dest_cond_eq (Thm.dest_arg ct)
   159     | _ => raise CTERM ("no equation", [ct]))
   159     | _ => raise CTERM ("no equation", [ct]))
   160 
   160 
   161   fun get_constrs thy (Type (n, _)) = these (Datatype_Data.get_constrs thy n)
   161   fun get_constrs thy (Type (n, _)) = these (Old_Datatype_Data.get_constrs thy n)
   162     | get_constrs _ _ = []
   162     | get_constrs _ _ = []
   163 
   163 
   164   fun is_constr thy (n, T) =
   164   fun is_constr thy (n, T) =
   165     let fun match (m, U) = m = n andalso Sign.typ_instance thy (T, U)
   165     let fun match (m, U) = m = n andalso Sign.typ_instance thy (T, U)
   166     in can (the o find_first match o get_constrs thy o Term.body_type) T end
   166     in can (the o find_first match o get_constrs thy o Term.body_type) T end