changeset 45906 | 0aaeb5520f2f |
parent 45891 | d73605c829cc |
child 46219 | 426ed18eba43 |
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Fri Dec 16 22:07:03 2011 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Sat Dec 17 12:10:37 2011 +0100 @@ -847,7 +847,7 @@ case T of TFree _ => NONE | Type (Tcon, _) => - (case Datatype_Data.get_constrs (Proof_Context.theory_of ctxt) Tcon of + (case Datatype.get_constrs (Proof_Context.theory_of ctxt) Tcon of NONE => NONE | SOME cs => (case strip_comb t of