src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
changeset 56254 a2dd9200854d
parent 56152 2a31945b9a58
child 56805 8a87502c7da3
     1.1 --- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Sat Mar 22 18:16:54 2014 +0100
     1.2 +++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Sat Mar 22 18:19:57 2014 +0100
     1.3 @@ -963,7 +963,7 @@
     1.4      val (bs, mxs) = map_split (apfst fst) fixes;
     1.5      val (arg_Ts, res_Ts) = map (strip_type o snd o fst #>> mk_tupleT_balanced) fixes |> split_list;
     1.6  
     1.7 -    val _ = (case filter_out (fn (_, T) => Sign.of_sort thy (T, HOLogic.typeS)) (bs ~~ arg_Ts) of
     1.8 +    val _ = (case filter_out (fn (_, T) => Sign.of_sort thy (T, @{sort type})) (bs ~~ arg_Ts) of
     1.9          [] => ()
    1.10        | (b, _) :: _ => primcorec_error ("type of " ^ Binding.print b ^ " contains top sort"));
    1.11