src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML
changeset 56254 a2dd9200854d
parent 56121 52e8f110fec3
child 56638 092a306bcc3d
     1.1 --- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Sat Mar 22 18:16:54 2014 +0100
     1.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Sat Mar 22 18:19:57 2014 +0100
     1.3 @@ -447,7 +447,7 @@
     1.4        | is_only_old_datatype _ = false;
     1.5  
     1.6      val _ = if exists is_only_old_datatype arg_Ts then raise OLD_PRIMREC () else ();
     1.7 -    val _ = (case filter_out (fn (_, T) => Sign.of_sort thy (T, HOLogic.typeS)) (bs ~~ res_Ts) of
     1.8 +    val _ = (case filter_out (fn (_, T) => Sign.of_sort thy (T, @{sort type})) (bs ~~ res_Ts) of
     1.9          [] => ()
    1.10        | (b, _) :: _ => raise PRIMREC ("type of " ^ Binding.print b ^ " contains top sort", []));
    1.11