src/HOL/BNF/Tools/bnf_lfp_rec_sugar.ML
changeset 54272 9d623cada37f
parent 54256 4843082be7ef
child 54851 48a24d371ebb
     1.1 --- a/src/HOL/BNF/Tools/bnf_lfp_rec_sugar.ML	Tue Nov 05 16:47:10 2013 +0100
     1.2 +++ b/src/HOL/BNF/Tools/bnf_lfp_rec_sugar.ML	Tue Nov 05 16:53:40 2013 +0100
     1.3 @@ -464,6 +464,8 @@
     1.4  
     1.5  fun prepare_primrec fixes specs lthy =
     1.6    let
     1.7 +    val thy = Proof_Context.theory_of lthy;
     1.8 +
     1.9      val (bs, mxs) = map_split (apfst fst) fixes;
    1.10      val fun_names = map Binding.name_of bs;
    1.11      val eqns_data = map (dissect_eqn lthy fun_names) specs;
    1.12 @@ -480,6 +482,10 @@
    1.13        |> map (partition_eq ((op =) o pairself #ctr))
    1.14        |> map (maps (map_filter (find_rec_calls has_call)));
    1.15  
    1.16 +    val _ = (case filter_out (fn (_, T) => Sign.of_sort thy (T, HOLogic.typeS)) (bs ~~ res_Ts) of
    1.17 +        [] => ()
    1.18 +      | (b, _) :: _ => primrec_error ("type of " ^ Binding.print b ^ " contains top sort"));
    1.19 +
    1.20      val ((n2m, rec_specs, _, induct_thm, induct_thms), lthy') =
    1.21        rec_specs_of bs arg_Ts res_Ts (get_indices fixes) callssss lthy;
    1.22