src/HOL/Tools/SMT/smt_normalize.ML
changeset 58112 8081087096ad
parent 58061 3d060f43accb
child 58132 6dcee1f6ea65
     1.1 --- a/src/HOL/Tools/SMT/smt_normalize.ML	Mon Sep 01 16:17:46 2014 +0200
     1.2 +++ b/src/HOL/Tools/SMT/smt_normalize.ML	Mon Sep 01 16:17:46 2014 +0200
     1.3 @@ -144,7 +144,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_Data.get_constrs thy n)
     1.8 +  fun get_constrs thy (Type (n, _)) = these (Old_Datatype_Data.get_constrs thy n)
     1.9      | get_constrs _ _ = []
    1.10  
    1.11    fun is_constr thy (n, T) =