--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon Sep 01 16:17:46 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon Sep 01 16:17:46 2014 +0200
@@ -1210,7 +1210,7 @@
is_some (fp_sugar_of no_defs_lthy bad_tc) then
error ("Inadmissible " ^ co_prefix fp ^ "recursive occurrence of type " ^ fake_T ^
" in type expression " ^ fake_T_backdrop)
- else if is_some (Datatype_Data.get_info (Proof_Context.theory_of no_defs_lthy)
+ else if is_some (Old_Datatype_Data.get_info (Proof_Context.theory_of no_defs_lthy)
bad_tc) then
error ("Unsupported " ^ co_prefix fp ^ "recursive occurrence of type " ^ fake_T ^
" via the old-style datatype " ^ quote bad_tc ^ " in type expression " ^