src/HOL/Tools/SMT/smt_normalize.ML
changeset 57996 ca917ea6969c
parent 56245 84fc7dfa3cd4
     1.1 --- a/src/HOL/Tools/SMT/smt_normalize.ML	Tue Aug 19 09:36:57 2014 +0200
     1.2 +++ b/src/HOL/Tools/SMT/smt_normalize.ML	Tue Aug 19 09:39:11 2014 +0200
     1.3 @@ -158,7 +158,7 @@
     1.4      | @{const HOL.implies} $ _ $ _ => dest_cond_eq (Thm.dest_arg ct)
     1.5      | _ => raise CTERM ("no equation", [ct]))
     1.6  
     1.7 -  fun get_constrs thy (Type (n, _)) = these (Datatype.get_constrs thy n)
     1.8 +  fun get_constrs thy (Type (n, _)) = these (Datatype_Data.get_constrs thy n)
     1.9      | get_constrs _ _ = []
    1.10  
    1.11    fun is_constr thy (n, T) =