# HG changeset patch
# User blanchet
# Date 1389272984 -3600
# Node ID f00012c2034405b7136270baf3115d699267609b
# Parent  26166d7f6a15b8cdfe70d0035c94033cf118dc8b
made 'datatype_new_compat' work with sort constraints

diff -r 26166d7f6a15 -r f00012c20344 src/HOL/BNF/Tools/bnf_lfp_compat.ML
--- a/src/HOL/BNF/Tools/bnf_lfp_compat.ML	Wed Jan 08 18:48:53 2014 +0100
+++ b/src/HOL/BNF/Tools/bnf_lfp_compat.ML	Thu Jan 09 14:09:44 2014 +0100
@@ -39,21 +39,19 @@
     val (fpT_names as fpT_name1 :: _) =
       map (fst o dest_Type o Proof_Context.read_type_name_proper lthy false) raw_fpT_names;
 
-    val Ss = Sign.arity_sorts thy fpT_name1 HOLogic.typeS;
-
-    val (unsorted_As, _) = lthy |> mk_TFrees (length Ss);
-    val As = map2 resort_tfree Ss unsorted_As;
-
     fun lfp_sugar_of s =
       (case fp_sugar_of lthy s of
         SOME (fp_sugar as {fp = Least_FP, ...}) => fp_sugar
       | _ => not_datatype s);
 
-    val {fp_res = {Ts = fpTs0, ...}, ...} = lfp_sugar_of fpT_name1;
+    val {ctr_sugars, ...} = lfp_sugar_of fpT_name1;
+    val fpTs0 as Type (_, var_As) :: _ = map (body_type o fastype_of o hd o #ctrs) ctr_sugars;
     val fpT_names' = map (fst o dest_Type) fpTs0;
 
     val _ = eq_set (op =) (fpT_names, fpT_names') orelse not_mutually_recursive fpT_names;
 
+    val (unsorted_As, _) = lthy |> mk_TFrees (length var_As);
+    val As = map2 (resort_tfree o Type.sort_of_atyp) var_As unsorted_As;
     val fpTs as fpT1 :: _ = map (fn s => Type (s, As)) fpT_names';
 
     fun add_nested_types_of (T as Type (s, _)) seen =