src/HOL/Tools/SMT/smt_normalize.ML
changeset 58132 6dcee1f6ea65
parent 58112 8081087096ad
child 59058 a78612c67ec0
     1.1 --- a/src/HOL/Tools/SMT/smt_normalize.ML	Mon Sep 01 19:28:00 2014 +0200
     1.2 +++ b/src/HOL/Tools/SMT/smt_normalize.ML	Mon Sep 01 19:57:48 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 (Old_Datatype_Data.get_constrs thy n)
     1.8 +  fun get_constrs thy (Type (n, _)) = these (BNF_LFP_Compat.get_constrs thy n)
     1.9      | get_constrs _ _ = []
    1.10  
    1.11    fun is_constr thy (n, T) =